Addition of a fixed natural to a canonical binary tape — proof internals

The proof follows the definition-level finite successor chain. Exact runs compose through seqTM; the all-prefix space induction uses the largest destination width rather than the total successor-chain runtime.

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

Canonical parked tape encoding of a natural for constant addition.

Equations

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

@[reducible, inline]

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

Predicate fixing the tapes framing a constant-addition execution.

Equations

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

theorem Complexity.TM.binaryAddConstTM_reachesIn_frame_internal {n : ℕ} (idx : Fin n) (constant dstValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hdst : (work₀ idx).HasBinaryNat dstValue) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i)) (hout : Parked out₀) : (binaryAddConstTM idx constant).reachesIn (binaryAddConstTime constant dstValue) { state := (binaryAddConstTM idx constant).qstart, input := inp₀, work := work₀, output := out₀ } { state := (binaryAddConstTM idx constant).qhalt, input := inp₀, work := Function.update work₀ idx (binaryAddConstNatTape (dstValue + constant)), output := out₀ }

theorem Complexity.TM.binaryAddConstTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (constant dstValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hdst : (work₀ idx).HasBinaryNat dstValue) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i)) (hout : Parked out₀) : (binaryAddConstTM idx constant).HoareTime (binaryAddConstFramePred inp₀ work₀ out₀) (binaryAddConstFramePred inp₀ (Function.update work₀ idx (binaryAddConstNatTape (dstValue + constant))) out₀) (binaryAddConstTime constant dstValue)

theorem Complexity.TM.binaryAddConstTM_hoareTimeSpace_frame_internal {n : ℕ} (idx : Fin n) (constant dstValue inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hdst : (work₀ idx).HasBinaryNat dstValue) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i)) (hout : Parked out₀) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (binaryAddConstTM idx constant).HoareTimeSpace (binaryAddConstFramePred inp₀ work₀ out₀) (binaryAddConstFramePred inp₀ (Function.update work₀ idx (binaryAddConstNatTape (dstValue + constant))) out₀) (binaryAddConstTime constant dstValue) inputLength (binaryAddConstSpace initialSpace constant dstValue)

theorem Complexity.TM.binaryAddConstTM_isTransducer_internal {n : ℕ} (idx : Fin n) (constant : ℕ) : (binaryAddConstTM idx constant).IsTransducer