The zero-extending increment — proof internals

⚠️ Unreviewed by Bolton

This file proves the exact full-frame execution of TM.binaryBumpTM, following the proof of TM.binaryBumpTM step for step: the two machines differ in one write. The carry proof is generalized over the already-zeroed low-order prefix, and everything it states is about the bit string on the tape — no number is involved, since a widening counter is not a numeral.

theorem Complexity.BinaryBump.steps_le_internal (bits : List Bool) : steps bits ≤ 2 * bits.length + 2

Internal worst-case bound for the exact step count.

Exact rewind and carry runs

Public-theorem internals

theorem Complexity.TM.binaryBumpTime_le_internal (bits : List Bool) : binaryBumpTime bits ≤ 2 * bits.length + 2

theorem Complexity.TM.binaryBumpTM_reachesIn_frame_internal {n : ℕ} (idx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hbits : (work₀ idx).HasBinaryString bits) (hcell0 : (work₀ idx).cells 0 = Γ.start) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (binaryBumpTM idx).Q), (binaryBumpTM idx).reachesIn (binaryBumpTime bits) { state := (binaryBumpTM idx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (binaryBumpTM idx).halted c' ∧ c'.input = inp₀ ∧ (∀ (i : Fin n), i ≠ idx → c'.work i = work₀ i) ∧ (c'.work idx).HasBinaryString (BinaryBump.bump bits) ∧ (c'.work idx).cells 0 = Γ.start ∧ c'.output = out₀

theorem Complexity.TM.binaryBumpTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (bits : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hbits : (work₀ idx).HasBinaryString bits) (hcell0 : (work₀ idx).cells 0 = Γ.start) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (binaryBumpTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ (work idx).HasBinaryString (BinaryBump.bump bits) ∧ (work idx).cells 0 = Γ.start ∧ out = out₀) (binaryBumpTime bits)

theorem Complexity.TM.binaryBumpTM_isTransducer_internal {n : ℕ} (idx : Fin n) : (binaryBumpTM idx).IsTransducer