Linear-time canonical binary subtraction -- composed semantics

This file composes the exact forward borrow scan with its backward canonicalization pass, then restores both preserved operands through the checked rewind tail. The complete machine computes natural-number monus, preserves the external tape frame literally, and carries explicit time and all-prefix auxiliary-space bounds.

def Complexity.TM.binaryRippleSubCorePost {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) : TapePred n

Postcondition at the end of the core binary ripple-subtraction phase.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.binaryRippleSubPost {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) : TapePred n

Postcondition for completed binary ripple subtraction.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.binaryRippleSubCoreTM_reachesIn_frame_internal {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 : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).Q), (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).reachesIn (binaryRippleSubCoreTime lhs.bits rhs.bits) { state := (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).halted c' ∧ binaryRippleSubCorePost lhsIdx rhsIdx resultIdx lhs rhs inp₀ work₀ out₀ c'.input c'.work c'.output

The direct core executes its forward and backward passes in exactly twice the larger operand width plus the two turn/bounce transitions.

theorem Complexity.TM.binaryRippleSubCoreTM_hoareTime_frame_internal {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 : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → (work₀ i).read ≠ Γ.start) (houtput : out₀.read ≠ Γ.start) : (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (binaryRippleSubCorePost lhsIdx rhsIdx resultIdx lhs rhs inp₀ work₀ out₀) (binaryRippleSubCoreTime lhs.bits rhs.bits)

Hoare-time form of the exact direct-core execution.

theorem Complexity.TM.binaryRippleSubTM_hoareTime_frame_internal {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₀) (binaryRippleSubPost lhsIdx rhsIdx resultIdx lhs rhs inp₀ work₀ out₀) (binaryRippleSubTime lhs rhs)

The complete direct subtraction machine restores both operands and returns canonical natural-number monus within the advertised width-linear bound.

theorem Complexity.TM.binaryRippleSubTM_hoareTimeSpace_frame_internal {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₀) (binaryRippleSubPost lhsIdx rhsIdx resultIdx lhs rhs inp₀ work₀ out₀) (binaryRippleSubTime lhs rhs) inputLength (initialSpace + binaryRippleSubTime lhs rhs)

Time-and-space contract for complete direct subtraction. The generic all-prefix envelope charges at most one additional cell per possible step.