Linear-time canonical binary subtraction

This module exposes a concrete three-tape ripple-borrow subtractor. It preserves two canonical little-endian operands, writes their truncated natural-number difference to a fresh zero result tape, restores every owned head to cell one, and preserves the complete external tape frame. Its running time is linear in the operand bit widths.

theorem Complexity.BinaryRippleSub.subtract_natBits (lhs rhs : ℕ) : subtract lhs.bits rhs.bits = (lhs - rhs).bits

Canonical ripple-borrow subtraction agrees with natural-number monus.

theorem Complexity.TM.binaryRippleSubTime_le (lhs rhs : ℕ) : binaryRippleSubTime lhs rhs ≤ 3 * (lhs.size + rhs.size) + 10

The complete subtractor has a linear bit-width envelope.

theorem Complexity.TM.binaryRippleSubTM_hoareTime_frame {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleSubDistinct lhsIdx rhsIdx resultIdx) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryNat lhs) (hrhs : (work₀ rhsIdx).HasBinaryNat rhs) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) : (binaryRippleSubTM lhsIdx rhsIdx resultIdx).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₀ ∧ (work lhsIdx).HasBinaryNat lhs ∧ (work rhsIdx).HasBinaryNat rhs ∧ (work resultIdx).HasBinaryNat (lhs - rhs) ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → work i = work₀ i) ∧ out = out₀) (binaryRippleSubTime lhs rhs)

Framed time contract for truncated subtraction. Both operands are restored, the initially-zero result becomes their natural-number difference, and every unrelated tape is preserved exactly.

theorem Complexity.TM.binaryRippleSubTM_reachesIn_frame {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleSubDistinct lhsIdx rhsIdx resultIdx) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryNat lhs) (hrhs : (work₀ rhsIdx).HasBinaryNat rhs) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) : ∃ (c' : Cfg n (binaryRippleSubTM lhsIdx rhsIdx resultIdx).Q), ∃ time ≤ binaryRippleSubTime lhs rhs, (binaryRippleSubTM lhsIdx rhsIdx resultIdx).reachesIn time { state := (binaryRippleSubTM lhsIdx rhsIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (binaryRippleSubTM lhsIdx rhsIdx resultIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work lhsIdx).HasBinaryNat lhs ∧ (c'.work rhsIdx).HasBinaryNat rhs ∧ (c'.work resultIdx).HasBinaryNat (lhs - rhs) ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → c'.work i = work₀ i) ∧ c'.output = out₀

Reachability form of the framed subtraction theorem.

theorem Complexity.TM.binaryRippleSubTM_hoareTimeSpace_frame {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleSubDistinct lhsIdx rhsIdx resultIdx) (lhs rhs inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ lhsIdx).HasBinaryNat lhs) (hrhs : (work₀ rhsIdx).HasBinaryNat rhs) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) (hinitial : { state := (binaryRippleSubTM lhsIdx rhsIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ }.WithinAuxSpace inputLength initialSpace) : (binaryRippleSubTM lhsIdx rhsIdx resultIdx).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₀ ∧ (work lhsIdx).HasBinaryNat lhs ∧ (work rhsIdx).HasBinaryNat rhs ∧ (work resultIdx).HasBinaryNat (lhs - rhs) ∧ (∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → work i = work₀ i) ∧ out = out₀) (binaryRippleSubTime lhs rhs) inputLength (initialSpace + binaryRippleSubTime lhs rhs)

All-prefix auxiliary-space contract obtained from the concrete linear time bound.

theorem Complexity.TM.binaryRippleSubTM_isTransducer {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : (binaryRippleSubTM lhsIdx rhsIdx resultIdx).IsTransducer

Canonical subtraction never moves the public output head left.