Linear-time canonical binary subtraction -- forward scan proof

This file proves the exact framed contract for the forward borrow scan, including its final turn into backward cleanup. Cleanup itself is proved in a separate internal layer.

theorem Complexity.TM.binaryRippleSubCoreTM_scan_reachesIn_frame_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleSubDistinct 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) : have raw := BinaryRippleSub.scan false lhs rhs; ∃ (c' : Cfg n (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).Q), (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).reachesIn (binaryRippleSubScanTime lhs rhs) { state := (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (c'.state = if raw.borrow = true then BinaryRippleSubPhase.erase else BinaryRippleSubPhase.trim false) ∧ 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).HasBinaryContent raw.bits ∧ (c'.work resultIdx).head = raw.bits.length ∧ (c'.work resultIdx).cells 0 = Γ.start ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → c'.work i = work₀ i) ∧ c'.output = out₀