Parked tape banks for fixed-time repetition

This internal module tracks exact preservation of every physical work tape not owned by the active repetition. Such tapes, and the real wrapper output tape, are parked off the left-end marker and remain unchanged under guarded idle transitions.

The invariant is established by setup, preserved through a complete positive- time run and its fixed rewind, and transferred across a nonfinal finish to the next active bank.

Main definitions and results

• NTM.RepeatOtherParked — all inactive work tapes and real output are parked
• NTM.RepeatOtherParked.parked — setup establishes the invariant
• NTM.RepeatOtherParked.trace_run — a complete positive-time run preserves it
• NTM.RepeatOtherParked.trace_rewind — the fixed rewind preserves it
• NTM.RepeatOtherParked.finish — a nonfinal finish transfers it to the next bank

def Complexity.NTM.RepeatOtherParked {n k T n✝ : ℕ} {tm : NTM n✝} (j : Fin k) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : Prop

Every physical work tape outside bank j, together with the real output tape, is parked off the start marker and satisfies the start invariant.

Equations

• Complexity.NTM.RepeatOtherParked j C = ((∀ (i : Fin (k * (n + 1))), (Complexity.NTM.repeatTapeCoord i).1 ≠ j → Complexity.NTM.RepeatParked (C.work i)) ∧ Complexity.NTM.RepeatParked C.output)

theorem Complexity.NTM.RepeatParked.writeAndMove_idle {t : Tape} (h : RepeatParked t) : t.writeAndMove (TM.readBackWrite t.read).toΓ (repeatSafeDir t.read (TM.idleDir t.read)) = t

A guarded idle write-and-move preserves a parked tape exactly.

theorem Complexity.NTM.repeatParked_parkedBlank : RepeatParked parkedBlank

The canonical parked blank tape satisfies RepeatParked.

theorem Complexity.NTM.repeatParked_parkedInput (x : List Bool) : RepeatParked (parkedInput x)

The canonical parked source input satisfies RepeatParked.

theorem Complexity.NTM.RepeatOtherParked.parked {n : ℕ} (tm : NTM n) (k T : ℕ) (x : List Bool) (j : Fin k) : RepeatOtherParked j (tm.repeatParkedCfg k T x)

The configuration after the first setup transition has every bank other than any designated active bank, and the real output, parked.

theorem Complexity.NTM.RepeatOtherParked.begin {n k T : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (choice : Fin 1 → Bool) : have j := ⟨0, hk⟩; RepeatOtherParked j ((tm.repeatAtTime k T).trace 1 choice (tm.repeatParkedCfg k T x))

The second setup transition activates bank zero and leaves every other bank and the real output parked.

theorem Complexity.NTM.RepeatOtherParked.run {n k T : ℕ} (tm : NTM n) {C : Cfg (k * (n + 1)) (tm.RepeatQ k T)} {j : Fin k} {t : Fin T} {q : tm.Q} {votes : Fin k → Bool} (hparked : RepeatOtherParked j C) (hstate : C.state = RepeatQ.run j t q votes) (choice : Fin 1 → Bool) : RepeatOtherParked j ((tm.repeatAtTime k T).trace 1 choice C)

One simulation slot preserves all parked tapes outside the active bank and the real output tape.

theorem Complexity.NTM.RepeatOtherParked.trace_run_prefix {n k T : ℕ} (tm : NTM n) (hT : 0 < T) (j : Fin k) (votes : Fin k → Bool) (choices : Fin T → Bool) (c₀ : Cfg n tm.Q) (C₀ : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hstate : C₀.state = RepeatQ.run j ⟨0, hT⟩ c₀.state votes) (hsim : tm.RepeatSimulates j c₀.state c₀ C₀) (hinp : C₀.input.StartInvariant) (hwork : ∀ (i : Fin (k * (n + 1))), (C₀.work i).StartInvariant) (hout : C₀.output.StartInvariant) (hparked : RepeatOtherParked j C₀) (m : ℕ) (hm : m ≤ T) : RepeatOtherParked j ((tm.repeatAtTime k T).trace m (fun (i : Fin m) => choices ⟨↑i, ⋯⟩) C₀)

Every prefix of a positive-time run preserves all parked tapes outside the active bank.

theorem Complexity.NTM.RepeatOtherParked.trace_run {n k T : ℕ} (tm : NTM n) (hT : 0 < T) (j : Fin k) (votes : Fin k → Bool) (choices : Fin T → Bool) (c₀ : Cfg n tm.Q) (C₀ : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hstate : C₀.state = RepeatQ.run j ⟨0, hT⟩ c₀.state votes) (hsim : tm.RepeatSimulates j c₀.state c₀ C₀) (hinp : C₀.input.StartInvariant) (hwork : ∀ (i : Fin (k * (n + 1))), (C₀.work i).StartInvariant) (hout : C₀.output.StartInvariant) (hparked : RepeatOtherParked j C₀) : RepeatOtherParked j ((tm.repeatAtTime k T).trace T choices C₀)

A complete positive-time simulation run preserves all parked tapes outside the active bank and the real output tape.

theorem Complexity.NTM.RepeatOtherParked.trace_rewind {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hstate : C.state = RepeatQ.rewind j ⟨0, ⋯⟩ q votes false fun (x : Fin (n + 1)) => false) (hinv : C.input.StartInvariant) (hactiveInv : ∀ (i : Fin (n + 1)), (C.work (repeatTapeIdx j i)).StartInvariant) (hinputHead : C.input.head ≤ T) (hactiveHead : ∀ (i : Fin (n + 1)), (C.work (repeatTapeIdx j i)).head ≤ T) (hparked : RepeatOtherParked j C) (choices : Fin (T + 1) → Bool) : RepeatOtherParked j ((tm.repeatAtTime k T).trace (T + 1) choices C)

The complete fixed rewind preserves every inactive parked tape and the real output tape.

theorem Complexity.NTM.RepeatOtherParked.finish {n k T : ℕ} (tm : NTM n) {C : Cfg (k * (n + 1)) (tm.RepeatQ k T)} {j : Fin k} {q : tm.Q} {votes : Fin k → Bool} (hparked : RepeatOtherParked j C) (hactive : ∀ (i : Fin (n + 1)), RepeatParked (C.work (repeatTapeIdx j i))) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (choice : Fin 1 → Bool) : have j' := ⟨↑j + 1, hj⟩; RepeatOtherParked j' ((tm.repeatAtTime k T).trace 1 choice C)

A nonfinal finish transfers the parked invariant to the next active bank, provided the just-completed active bank has been parked by fixed rewind.