Linear-time canonical binary subtraction -- backward cleanup

This module proves the exact backward half of TM.binaryRippleSubCoreTM. Underflow erases the entire fixed-width result. Otherwise the machine erases only redundant high zeros, preserves the significant suffix after its first high one, and returns the result head to cell one. All other tapes are framed literally throughout the run.

theorem Complexity.Tape.HasBinaryContent.write_blank_last_internal {t : Tape} {bitsPrefix : List Bool} {bit : Bool} (h : t.HasBinaryContent (bitsPrefix ++ [bit])) (hhead : t.head = bitsPrefix.length + 1) : (t.write Γ.blank).HasBinaryContent bitsPrefix

Blanking the final represented cell shortens canonical binary contents by one bit. The erased bit may have either value.

Exact backward runs

theorem Complexity.TM.binaryRippleSubCoreTM_cleanup_run_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (raw : List Bool) (borrow : Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ resultIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) (hcontent : (work₀ resultIdx).HasBinaryContent raw) (hcell0 : (work₀ resultIdx).cells 0 = Γ.start) (hhead : (work₀ resultIdx).head = raw.length) : ∃ (c' : Cfg n (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).Q), (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).reachesIn (raw.length + 1) { state := if borrow = true then BinaryRippleSubPhase.erase else BinaryRippleSubPhase.trim false, input := inp₀, work := work₀, output := out₀ } c' ∧ (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).halted c' ∧ c'.input = inp₀ ∧ (∀ (i : Fin n), i ≠ resultIdx → c'.work i = work₀ i) ∧ (c'.work resultIdx).HasBinaryString (if borrow = true then [] else BinaryRippleSub.trimHighZeros raw) ∧ (c'.work resultIdx).cells 0 = Γ.start ∧ c'.output = out₀

Exact framed backward cleanup after the forward scan has turned the result head left. A final borrow erases the entire raw result; otherwise all and only its redundant high zeros are erased.