Canonical binary multiply-add

This module exposes a nested repeated-addition machine over five pairwise-distinct canonical binary work tapes. It preserves both operands, updates only the accumulator, and restores both private counters to canonical zero. The resource contract gives a width-based all-prefix space bound.

Main results

• binaryMulAddIntoTM_hoareTime_frame gives the literal endpoint and time bound.
• binaryMulAddIntoTM_hoareTimeSpace_frame adds the all-prefix space bound.
• binaryMulAddIntoTM_isTransducer proves append-only-output safety.

theorem Complexity.TM.binaryMulAddIntoTM_hoareTime_frame {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) (hdistinct : BinaryMulAddDistinct leftIdx rightIdx accIdx mulCounterIdx addCounterIdx) (leftValue rightValue accValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hleft : (work₀ leftIdx).HasBinaryNat leftValue) (hright : (work₀ rightIdx).HasBinaryNat rightValue) (hacc : (work₀ accIdx).HasBinaryNat accValue) (hmulCounter : (work₀ mulCounterIdx).HasBinaryNat 0) (haddCounter : (work₀ addCounterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ leftIdx → i ≠ rightIdx → i ≠ accIdx → i ≠ mulCounterIdx → i ≠ addCounterIdx → Parked (work₀ i)) (hout : Parked out₀) : (binaryMulAddIntoTM leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).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₀ accIdx ((Tape.init (List.map Γ.ofBool (accValue + leftValue * rightValue).bits)).move Dir3.right) ∧ out = out₀) (binaryMulAddTime leftValue rightValue accValue)

Multiply-add changes only the accumulator, from accValue to accValue + leftValue * rightValue; both operands and both zero counters are restored literally.

theorem Complexity.TM.binaryMulAddIntoTM_hoareTimeSpace_frame {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) (hdistinct : BinaryMulAddDistinct leftIdx rightIdx accIdx mulCounterIdx addCounterIdx) (leftValue rightValue accValue inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hleft : (work₀ leftIdx).HasBinaryNat leftValue) (hright : (work₀ rightIdx).HasBinaryNat rightValue) (hacc : (work₀ accIdx).HasBinaryNat accValue) (hmulCounter : (work₀ mulCounterIdx).HasBinaryNat 0) (haddCounter : (work₀ addCounterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ leftIdx → i ≠ rightIdx → i ≠ accIdx → i ≠ mulCounterIdx → i ≠ addCounterIdx → Parked (work₀ i)) (hout : Parked out₀) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (binaryMulAddIntoTM leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).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₀ accIdx ((Tape.init (List.map Γ.ofBool (accValue + leftValue * rightValue).bits)).move Dir3.right) ∧ out = out₀) (binaryMulAddTime leftValue rightValue accValue) inputLength (binaryMulAddSpace initialSpace leftValue rightValue accValue)

Time-and-space multiply-add contract. Every reachable configuration stays within the stated width-based bound.

theorem Complexity.TM.binaryMulAddIntoTM_isTransducer {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) : (binaryMulAddIntoTM leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).IsTransducer

Binary multiply-add never moves its output head left.