Linear-time canonical binary addition -- scan proof

This file proves the exact operational contract for the carry-bearing forward scan. Rewinding and the complete canonical-natural interface are composed in later internal layers.

theorem Complexity.TM.binaryRippleAddScanTM_reachesIn_frame_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleAddDistinct lhsIdx rhsIdx resultIdx) (lhs rhs : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryString lhs) (hrhs : (work₀ rhsIdx).HasBinaryString rhs) (hresult : (work₀ resultIdx).HasBinaryPrefix []) (hresultStart : (work₀ resultIdx).cells 0 = Γ.start) (hinput : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (binaryRippleAddScanTM lhsIdx rhsIdx resultIdx).Q), (binaryRippleAddScanTM lhsIdx rhsIdx resultIdx).reachesIn (binaryRippleAddScanTime lhs rhs) { state := (binaryRippleAddScanTM lhsIdx rhsIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (binaryRippleAddScanTM lhsIdx rhsIdx resultIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work lhsIdx).cells = (work₀ lhsIdx).cells ∧ (c'.work lhsIdx).head = lhs.length + 1 ∧ (c'.work rhsIdx).cells = (work₀ rhsIdx).cells ∧ (c'.work rhsIdx).head = rhs.length + 1 ∧ (c'.work resultIdx).HasBinaryPrefix (BinaryRippleAdd.ripple false lhs rhs) ∧ (c'.work resultIdx).cells 0 = Γ.start ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → c'.work i = work₀ i) ∧ c'.output = out₀