Fixed-time rewind correctness for PTM repetition

This internal module lifts the one-tape fixed-rewind theorem to the complete NTM.repeatAtTime wrapper configuration. A snapshot packages the input tape, all work-tape banks, the real output tape, and the per-tape completion flags. Its deterministic step commutes with one wrapper .rewind transition.

After exactly T + 1 rewind transitions, every active tape is parked at cell one with its contents unchanged, the control enters .finish, and the inactive tapes and real output tape are exactly preserved. Choice bits are arbitrary in this administrative phase.

Main definitions and results

• NTM.RepeatRewindSnapshot — simultaneous tape-and-flag rewind state
• NTM.repeatRewindSnapshotStep, NTM.repeatRewindSnapshotIter — pure dynamics
• NTM.repeatAtTime_trace_one_rewind — one wrapper step matches one snapshot step
• NTM.repeatAtTime_trace_rewind_snapshot — exact T + 1 snapshot correspondence
• NTM.repeatAtTime_trace_rewind_bound — finish state, parked active tapes, frame

structure Complexity.NTM.RepeatRewindSnapshot (n k : ℕ) : Type

Pure data advanced during the simultaneous fixed rewind of one repetition bank. The control state and completed-run votes remain external constants.

• input : Tape

  Shared read-only input tape.

• work : Fin (k * (n + 1)) → Tape

  All physical work-tape banks.

• output : Tape

  Real wrapper output tape, framed throughout rewind.

• inputDone : Bool

  Whether the input head has already bounced from cell zero.

• bankDone : Fin (n + 1) → Bool

  Per-local-tape bounce flags for the active bank.

def Complexity.NTM.RepeatParked (t : Tape) : Prop

A framed tape is off the start marker and satisfies its uniqueness invariant, hence the wrapper's idle action preserves it exactly.

Equations

• Complexity.NTM.RepeatParked t = (t.StartInvariant ∧ 1 ≤ t.head)

def Complexity.NTM.RepeatRewindSnapshot.WellFormed {k n : ℕ} (j : Fin k) (S : RepeatRewindSnapshot n k) : Prop

Snapshot well-formedness: input and active tapes satisfy the start-marker invariant, while inactive tapes and real output are parked for exact framing.

Equations

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

def Complexity.NTM.repeatRewindSnapshotStep {k n : ℕ} (j : Fin k) (S : RepeatRewindSnapshot n k) : RepeatRewindSnapshot n k

Advance every active tape and completion flag by one fixed rewind step.

Equations

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

def Complexity.NTM.repeatRewindSnapshotIter {k n : ℕ} (j : Fin k) : ℕ → RepeatRewindSnapshot n k → RepeatRewindSnapshot n k

Iterate the simultaneous rewind snapshot dynamics.

Equations

• Complexity.NTM.repeatRewindSnapshotIter j 0 x✝ = x✝
• Complexity.NTM.repeatRewindSnapshotIter j m.succ x✝ = Complexity.NTM.repeatRewindSnapshotIter j m (Complexity.NTM.repeatRewindSnapshotStep j x✝)

@[simp]

theorem Complexity.NTM.repeatRewindBankDone_apply {k n : ℕ} (work : Fin (k * (n + 1)) → Tape) (j : Fin k) (done : Fin (n + 1) → Bool) : repeatRewindBankDone (fun (i : Fin (k * (n + 1))) => (work i).read) j done = fun (i : Fin (n + 1)) => repeatRewindDone (done i) (work (repeatTapeIdx j i)).read

Pointwise form of repeatRewindBankDone on tape reads.

def Complexity.NTM.repeatRewindCfg {n k T : ℕ} (tm : NTM n) (j : Fin k) (r : Fin (T + 1)) (q : tm.Q) (votes : Fin k → Bool) (S : RepeatRewindSnapshot n k) : Cfg (k * (n + 1)) (tm.RepeatQ k T)

Embed a rewind snapshot at counter r into the wrapper configuration.

Equations

• tm.repeatRewindCfg j r q votes S = { state := Complexity.NTM.RepeatQ.rewind j r q votes S.inputDone S.bankDone, input := S.input, work := S.work, output := S.output }

def Complexity.NTM.repeatFinishCfg {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (S : RepeatRewindSnapshot n k) : Cfg (k * (n + 1)) (tm.RepeatQ k T)

Embed a completed rewind snapshot in the wrapper's finish state.

Equations

• tm.repeatFinishCfg j q votes S = { state := Complexity.NTM.RepeatQ.finish j q votes, input := S.input, work := S.work, output := S.output }

theorem Complexity.NTM.repeatFixedRewindTapeStep_fst_eq_move (t : Tape) (done : Bool) (h : t.StartInvariant) : (repeatFixedRewindTapeStep (t, done)).1 = t.move (repeatSafeDir t.read (repeatRewindDir done t.read))

The tape component of repeatFixedRewindTapeStep is its guarded movement: writing the current symbol back is cell-preserving under StartInvariant.

theorem Complexity.NTM.repeatRewindSnapshotStep_wellFormed {k n : ℕ} (j : Fin k) (S : RepeatRewindSnapshot n k) (h : RepeatRewindSnapshot.WellFormed j S) : RepeatRewindSnapshot.WellFormed j (repeatRewindSnapshotStep j S)

One simultaneous snapshot step preserves snapshot well-formedness.

theorem Complexity.NTM.repeatRewindSnapshotIter_wellFormed {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) (h : RepeatRewindSnapshot.WellFormed j S) : RepeatRewindSnapshot.WellFormed j (repeatRewindSnapshotIter j m S)

Every finite snapshot iteration preserves well-formedness.

theorem Complexity.NTM.repeatRewindSnapshotStep_iter {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) : repeatRewindSnapshotStep j (repeatRewindSnapshotIter j m S) = repeatRewindSnapshotIter j m (repeatRewindSnapshotStep j S)

A snapshot step commutes with any number of iterations of itself.

theorem Complexity.NTM.repeatRewindSnapshotIter_succ_snoc {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) : repeatRewindSnapshotStep j (repeatRewindSnapshotIter j m S) = repeatRewindSnapshotIter j (m + 1) S

Snoc form of the snapshot iterator recursion.

theorem Complexity.NTM.repeatRewindSnapshotIter_input {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) : ((repeatRewindSnapshotIter j m S).input, (repeatRewindSnapshotIter j m S).inputDone) = repeatFixedRewindTapeIter m (S.input, S.inputDone)

The input tape and flag project to the pure one-tape rewind iterator.

theorem Complexity.NTM.repeatRewindSnapshotIter_active {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) (i : Fin (n + 1)) : ((repeatRewindSnapshotIter j m S).work (repeatTapeIdx j i), (repeatRewindSnapshotIter j m S).bankDone i) = repeatFixedRewindTapeIter m (S.work (repeatTapeIdx j i), S.bankDone i)

Each active bank tape and flag project to the pure one-tape iterator.

theorem Complexity.NTM.repeatRewindSnapshotIter_inactive {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) (i : Fin (k * (n + 1))) (hi : (repeatTapeCoord i).1 ≠ j) : (repeatRewindSnapshotIter j m S).work i = S.work i

Snapshot iteration preserves every inactive physical work tape exactly.

@[simp]

theorem Complexity.NTM.repeatRewindSnapshotIter_output {k n : ℕ} (j : Fin k) (m : ℕ) (S : RepeatRewindSnapshot n k) : (repeatRewindSnapshotIter j m S).output = S.output

Snapshot iteration preserves the real output tape exactly.

theorem Complexity.NTM.repeatAtTime_trace_one_rewind {n k T : ℕ} (tm : NTM n) (j : Fin k) (r : Fin (T + 1)) (q : tm.Q) (votes : Fin k → Bool) (S : RepeatRewindSnapshot n k) (hS : RepeatRewindSnapshot.WellFormed j S) (choice : Fin 1 → Bool) : (tm.repeatAtTime k T).trace 1 choice (tm.repeatRewindCfg j r q votes S) = if hr : ↑r + 1 < T + 1 then tm.repeatRewindCfg j ⟨↑r + 1, hr⟩ q votes (repeatRewindSnapshotStep j S) else tm.repeatFinishCfg j q votes (repeatRewindSnapshotStep j S)

One wrapper rewind transition commutes with one simultaneous snapshot step. The choice bit is arbitrary because the administrative phase ignores it.

theorem Complexity.NTM.repeatAtTime_trace_rewind_prefix {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (S : RepeatRewindSnapshot n k) (hS : RepeatRewindSnapshot.WellFormed j S) (m : ℕ) (hm : m < T + 1) (choices : Fin m → Bool) : (tm.repeatAtTime k T).trace m choices (tm.repeatRewindCfg j ⟨0, ⋯⟩ q votes S) = tm.repeatRewindCfg j ⟨m, hm⟩ q votes (repeatRewindSnapshotIter j m S)

Before the final rewind slot, an m-step wrapper trace agrees exactly with m pure snapshot steps and carries rewind counter m.

theorem Complexity.NTM.repeatAtTime_trace_rewind_snapshot {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (S : RepeatRewindSnapshot n k) (hS : RepeatRewindSnapshot.WellFormed j S) (choices : Fin (T + 1) → Bool) : (tm.repeatAtTime k T).trace (T + 1) choices (tm.repeatRewindCfg j ⟨0, ⋯⟩ q votes S) = tm.repeatFinishCfg j q votes (repeatRewindSnapshotIter j (T + 1) S)

Exactly T + 1 wrapper rewind transitions produce the finish configuration associated with T + 1 simultaneous snapshot steps.

theorem Complexity.NTM.repeatAtTime_trace_rewind_bound {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) (hinactive : ∀ (i : Fin (k * (n + 1))), (repeatTapeCoord i).1 ≠ j → RepeatParked (C.work i)) (hout : RepeatParked C.output) (choices : Fin (T + 1) → Bool) : have C' := (tm.repeatAtTime k T).trace (T + 1) choices C; C'.state = RepeatQ.finish j q votes ∧ C'.input.head = 1 ∧ C'.input.cells = C.input.cells ∧ (∀ (i : Fin (n + 1)), (C'.work (repeatTapeIdx j i)).head = 1 ∧ (C'.work (repeatTapeIdx j i)).cells = (C.work (repeatTapeIdx j i)).cells) ∧ (∀ (i : Fin (k * (n + 1))), (repeatTapeCoord i).1 ≠ j → C'.work i = C.work i) ∧ C'.output = C.output

Fixed rewind correctness. Starting from rewind counter zero with all completion flags false, T + 1 administrative steps enter .finish, park the input and every active-bank tape at cell one without changing their cells, and preserve every inactive tape and the real output tape exactly.