Little-endian binary predecessor — proof internals

This file proves pure ripple-borrow semantics and the exact full-frame execution of TM.binaryPredTM. The machine proof tracks the already-borrowed low-order prefix independently of the target head, including the canonical high-bit erasure needed when decrementing a power of two.

theorem Complexity.BinaryPred.ripple_succ_natBits_internal (value : ℕ) : ripple (value + 1).bits = value.bits

Internal proof that ripple borrow on a positive canonical value computes its predecessor.

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

Internal worst-case bound for predecessor's exact transition count.

Exact rewind and borrow runs

Public-theorem internals

theorem Complexity.TM.binaryPredTime_le_internal (value : ℕ) : binaryPredTime value ≤ 2 * (value + 1).size + 2

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

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

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

theorem Complexity.TM.binaryPredTM_isTransducer_internal {n : ℕ} (idx : Fin n) : (binaryPredTM idx).IsTransducer