Little-endian binary successor — proof internals

This file proves the pure ripple semantics and the exact full-frame execution of TM.binarySuccTM. The carry proof uses a private head-independent binary content predicate, generalized over the already-zeroed low-order prefix.

theorem Complexity.BinarySucc.ripple_natBits_internal (value : ℕ) : ripple value.bits = (value + 1).bits

Internal proof that ripple carry computes successor on canonical little-endian natural-number bits.

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

Internal worst-case bound for the exact successor step count.

Exact rewind and carry runs

Public-theorem internals

theorem Complexity.TM.binarySuccTime_le_internal (value : ℕ) : binarySuccTime value ≤ 2 * value.size + 2

theorem Complexity.TM.binarySuccTM_reachesIn_frame_internal {n : ℕ} (idx : Fin n) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (binarySuccTM idx).Q), (binarySuccTM idx).reachesIn (binarySuccTime value) { state := (binarySuccTM idx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (binarySuccTM idx).halted c' ∧ c'.input = inp₀ ∧ (∀ (i : Fin n), i ≠ idx → c'.work i = work₀ i) ∧ (c'.work idx).HasBinaryNat (value + 1) ∧ c'.output = out₀

theorem Complexity.TM.binarySuccTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (binarySuccTM 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).HasBinaryNat (value + 1) ∧ out = out₀) (binarySuccTime value)

theorem Complexity.TM.binarySuccTM_hoareTimeSpace_frame_internal {n : ℕ} (idx : Fin n) (value inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) (hinitial : { state := (binarySuccTM idx).qstart, input := inp₀, work := work₀, output := out₀ }.WithinAuxSpace inputLength initialSpace) : (binarySuccTM idx).HoareTimeSpace (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).HasBinaryNat (value + 1) ∧ out = out₀) (binarySuccTime value) inputLength (initialSpace + binarySuccTime value)

theorem Complexity.TM.binarySuccTM_isTransducer_internal {n : ℕ} (idx : Fin n) : (binarySuccTM idx).IsTransducer