Stable bounded decoding of terminated bit prefixes

Proved

CookLevin.readBits_prefix_terminated_append_layer

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

bit-stringscook-levinturing-machines

A tape segment that contains exactly a Boolean word $x$ from a base cell and a non-bit terminator immediately afterward is decoded by readBits as $x$ for every sufficiently large fuel value. Moreover, if one Boolean bit $b$ is written after the prefix and a non-bit terminator is placed after that bit, every sufficiently large bounded read returns $x \,\mathbin{++}\, [b]$ . This packages the output-prefix and terminator invariant needed for safe clock padding and append-bit postprocessing.

Preamble

import Definitions.Def_CookLevin_Cost
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.readBits_prefix_terminated_append_layer :
    (∀ (tape : Nat → Symbol) (base : Nat) (xs : List Bool),
      ((∀ j, j < xs.length → tape (base + j) = boolSym xs[j]!) ∧
        symBool? (tape (base + xs.length)) = none) →
      ∀ extra : Nat, readBits (xs.length + 1 + extra) tape base = xs) ∧
    (∀ (tape : Nat → Symbol) (base : Nat) (xs : List Bool) (b : Bool),
      (∀ j, j < xs.length → tape (base + j) = boolSym xs[j]!) →
      tape (base + xs.length) = boolSym b →
      symBool? (tape (base + xs.length + 1)) = none →
      ∀ extra : Nat,
        readBits ((xs ++ [b]).length + 1 + extra) tape base = xs ++ [b]) := by sorry

View graph