Canonical binary addition

This module exposes binary addition assembled from the canonical count-up loop and binary successor. Three pairwise-distinct work tapes hold a preserved source, an updated destination, and scratch counter. The scratch tape starts at canonical zero and is restored literally after the addition.

The endpoint is a full frame equality: only the destination tape changes, from dstValue to dstValue + srcValue. The all-prefix space theorem is width-based rather than derived from total loop runtime.

Main results

• binaryAddLoopTM_reachesIn_frame gives the exact loop runtime and endpoint.
• binaryAddIntoTM_hoareTime_frame restores scratch zero with a full frame.
• binaryAddIntoTM_hoareTimeSpace_frame adds an all-prefix space bound.
• binaryAddIntoTM_isTransducer proves append-only-output safety.

theorem Complexity.TM.binaryAddLoopTM_reachesIn_frame {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) (hsrcDst : srcIdx ≠ dstIdx) (hsrcCounter : srcIdx ≠ counterIdx) (hdstCounter : dstIdx ≠ counterIdx) (srcValue dstValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrc : (work₀ srcIdx).HasBinaryNat srcValue) (hdst : (work₀ dstIdx).HasBinaryNat dstValue) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ srcIdx → i ≠ dstIdx → i ≠ counterIdx → Parked (work₀ i)) (hout : Parked out₀) : (binaryAddLoopTM srcIdx dstIdx counterIdx).reachesIn (binaryAddLoopTime srcValue dstValue) { state := (binaryAddLoopTM srcIdx dstIdx counterIdx).qstart, input := inp₀, work := work₀, output := out₀ } { state := (binaryAddLoopTM srcIdx dstIdx counterIdx).qhalt, input := inp₀, work := Function.update (Function.update work₀ dstIdx ((Tape.init (List.map Γ.ofBool (dstValue + srcValue).bits)).move Dir3.right)) counterIdx ((Tape.init (List.map Γ.ofBool srcValue.bits)).move Dir3.right), output := out₀ }

The addition loop has an exact runtime and literal endpoint. It preserves the source and external frame, increments the destination by srcValue, and leaves the scratch counter equal to srcValue.

theorem Complexity.TM.binaryAddIntoTM_hoareTime_frame {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) (hsrcDst : srcIdx ≠ dstIdx) (hsrcCounter : srcIdx ≠ counterIdx) (hdstCounter : dstIdx ≠ counterIdx) (srcValue dstValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrc : (work₀ srcIdx).HasBinaryNat srcValue) (hdst : (work₀ dstIdx).HasBinaryNat dstValue) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ srcIdx → i ≠ dstIdx → i ≠ counterIdx → Parked (work₀ i)) (hout : Parked out₀) : (binaryAddIntoTM srcIdx dstIdx counterIdx).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 = Function.update work₀ dstIdx ((Tape.init (List.map Γ.ofBool (dstValue + srcValue).bits)).move Dir3.right) ∧ out = out₀) (binaryAddTime srcValue dstValue)

Addition changes only the destination tape, from dstValue to dstValue + srcValue. In particular, source, scratch zero, input, output, and every unrelated work tape are restored literally.

theorem Complexity.TM.binaryAddIntoTM_hoareTimeSpace_frame {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) (hsrcDst : srcIdx ≠ dstIdx) (hsrcCounter : srcIdx ≠ counterIdx) (hdstCounter : dstIdx ≠ counterIdx) (srcValue dstValue inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hsrc : (work₀ srcIdx).HasBinaryNat srcValue) (hdst : (work₀ dstIdx).HasBinaryNat dstValue) (hcounter : (work₀ counterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ srcIdx → i ≠ dstIdx → i ≠ counterIdx → Parked (work₀ i)) (hout : Parked out₀) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (binaryAddIntoTM srcIdx dstIdx counterIdx).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 = Function.update work₀ dstIdx ((Tape.init (List.map Γ.ofBool (dstValue + srcValue).bits)).move Dir3.right) ∧ out = out₀) (binaryAddTime srcValue dstValue) inputLength (binaryAddSpace initialSpace srcValue dstValue)

Time-and-space form of binaryAddIntoTM_hoareTime_frame. Every reachable configuration stays within binaryAddSpace; the bound depends on the source and final-destination binary widths, not on the total iteration count.

theorem Complexity.TM.binaryAddIntoTM_isTransducer {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : (binaryAddIntoTM srcIdx dstIdx counterIdx).IsTransducer

Binary addition never moves its output head left.