Canonical binary addition — proof internals

The proof instantiates BinaryForLoopSpec with binary successor on the destination. Concrete work-tape families record both the destination and scratch counter after every iteration. The prefix-space certificate reasons about one comparison or one iteration at a time, avoiding any dependence on the total number of loop iterations.

def Complexity.TM.binaryAddNatTape (value : ℕ) : Tape

The standard parked tape for one canonical binary natural.

Equations

• Complexity.TM.binaryAddNatTape value = (Complexity.Tape.init (List.map Complexity.Γ.ofBool value.bits)).move Complexity.Dir3.right

def Complexity.TM.binaryAddWorkAt {n : ℕ} (work : Fin n → Tape) (dstIdx counterIdx : Fin n) (dstValue current : ℕ) : Fin n → Tape

Work tapes after current completed addition iterations.

Equations

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

@[reducible, inline]

abbrev Complexity.TM.binaryAddFramePred {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) : TapePred n

Predicate fixing the tapes framing a binary-addition execution.

Equations

• Complexity.TM.binaryAddFramePred inp₀ work₀ out₀ inp work out = (inp = inp₀ ∧ work = work₀ ∧ out = out₀)

theorem Complexity.TM.binaryAddLoopTM_reachesIn_frame_internal {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 := binaryAddWorkAt work₀ dstIdx counterIdx dstValue srcValue, output := out₀ }

The count-up addition loop has an exact runtime and complete endpoint.

theorem Complexity.TM.binaryAddIntoTM_hoareTime_frame_internal {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 (binaryAddFramePred inp₀ work₀ out₀) (binaryAddFramePred inp₀ (Function.update work₀ dstIdx (binaryAddNatTape (dstValue + srcValue))) out₀) (binaryAddTime srcValue dstValue)

Binary addition restores scratch zero and preserves the complete external frame within the stated time bound.

theorem Complexity.TM.binaryAddIntoTM_hoareTimeSpace_frame_internal {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 (binaryAddFramePred inp₀ work₀ out₀) (binaryAddFramePred inp₀ (Function.update work₀ dstIdx (binaryAddNatTape (dstValue + srcValue))) out₀) (binaryAddTime srcValue dstValue) inputLength (binaryAddSpace initialSpace srcValue dstValue)

Binary addition has an honest all-prefix space bound controlled by binary widths rather than total loop runtime.

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

Binary addition never moves its output head left.