Fresh-bank frame invariants for fixed-time repetition

This internal layer tracks the parts of a repetition configuration not owned by the active trial. It proves that input contents, strictly future tape banks, and the real output tape survive simulation and rewind steps, and that a nonfinal finish transition initializes the next trial exactly at the source machine's initial configuration.

Main results

• NTM.RepeatFrame — invariant for input cells, future banks, and real output
• NTM.RepeatFrame.run, .rewind, .finish — one-step frame preservation
• NTM.RepeatFrame.finish_next_project — exact next-trial initialization

def Complexity.NTM.parkedBlank : Tape

A blank tape parked at cell one.

Equations

• Complexity.NTM.parkedBlank = (Complexity.Tape.init []).move Complexity.Dir3.right

def Complexity.NTM.parkedInput (x : List Bool) : Tape

The source input tape parked at cell one.

Equations

• Complexity.NTM.parkedInput x = (Complexity.Tape.init (List.map Complexity.Γ.ofBool x)).move Complexity.Dir3.right

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

Frame facts not owned by the currently active trial: input contents stay unchanged, every strictly later bank is still parked and blank, and the real output is still parked and blank.

Equations

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

@[simp]

theorem Complexity.NTM.parkedBlank_read : parkedBlank.read = Γ.blank

The parked blank tape reads blank.

@[simp]

theorem Complexity.NTM.parkedBlank_head : parkedBlank.head = 1

The parked blank tape's head is at cell one.

theorem Complexity.NTM.parkedBlank_write_idle : parkedBlank.writeAndMove (TM.readBackWrite parkedBlank.read).toΓ (repeatSafeDir parkedBlank.read (TM.idleDir parkedBlank.read)) = parkedBlank

A guarded idle write-and-move preserves the parked blank tape.

@[simp]

theorem Complexity.NTM.parkedBlank_guardedIdle : parkedBlank.writeAndMove Γ.blank (repeatSafeDir Γ.blank (TM.idleDir Γ.blank)) = parkedBlank

Reduced form of guarded idle preservation for the parked blank tape.

theorem Complexity.NTM.parkedBlank_position : parkedBlank.writeAndMove (TM.readBackWrite parkedBlank.read).toΓ (repeatSafeDir parkedBlank.read (TM.moveLeftDir parkedBlank.read)) = Tape.init []

Positioning a parked blank tape reconstructs the initial blank tape.

theorem Complexity.NTM.parkedInput_position (x : List Bool) : (parkedInput x).writeAndMove (TM.readBackWrite (parkedInput x).read).toΓ (repeatSafeDir (parkedInput x).read (TM.moveLeftDir (parkedInput x).read)) = Tape.init (List.map Γ.ofBool x)

Positioning a parked input with write-back reconstructs the initial input.

theorem Complexity.NTM.parkedInput_move_position (x : List Bool) : (parkedInput x).move (repeatSafeDir (parkedInput x).read (TM.moveLeftDir (parkedInput x).read)) = Tape.init (List.map Γ.ofBool x)

Positioning the read-only parked input reconstructs the initial input.

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

The configuration after setup satisfies the frame for every trial index.

theorem Complexity.NTM.trace_one_input_cells {n k T : ℕ} (tm : NTM n) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (choice : Fin 1 → Bool) : ((tm.repeatAtTime k T).trace 1 choice C).input.cells = C.input.cells

Every wrapper transition preserves the cells of the read-only input tape.

theorem Complexity.NTM.trace_setup_frame {n k T : ℕ} (tm : NTM n) (x : List Bool) (j : Fin k) (choice : Fin 1 → Bool) : RepeatFrame x j ((tm.repeatAtTime k T).trace 1 choice ((tm.repeatAtTime k T).initCfg x))

The setup transition establishes the frame for any prospective first trial.

theorem Complexity.NTM.trace_run_inactive_bank {n k T : ℕ} (tm : NTM n) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (j l : Fin k) (t : Fin T) (q : tm.Q) (votes : Fin k → Bool) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.run j t q votes) (hne : l ≠ j) (hparked : ∀ (i : Fin (n + 1)), C.work (repeatTapeIdx l i) = parkedBlank) (i : Fin (n + 1)) : ((tm.repeatAtTime k T).trace 1 choice C).work (repeatTapeIdx l i) = parkedBlank

A simulation transition leaves every inactive parked bank unchanged.

theorem Complexity.NTM.trace_rewind_inactive_bank {n k T : ℕ} (tm : NTM n) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (j l : Fin k) (r : Fin (T + 1)) (q : tm.Q) (votes : Fin k → Bool) (inputDone : Bool) (bankDone : Fin (n + 1) → Bool) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.rewind j r q votes inputDone bankDone) (hne : l ≠ j) (hparked : ∀ (i : Fin (n + 1)), C.work (repeatTapeIdx l i) = parkedBlank) (i : Fin (n + 1)) : ((tm.repeatAtTime k T).trace 1 choice C).work (repeatTapeIdx l i) = parkedBlank

A rewind transition leaves every inactive parked bank unchanged.

theorem Complexity.NTM.trace_finish_future_bank {n k T : ℕ} (tm : NTM n) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (j l : Fin k) (q : tm.Q) (votes : Fin k → Bool) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hl : ↑j + 1 < ↑l) (hparked : ∀ (i : Fin (n + 1)), C.work (repeatTapeIdx l i) = parkedBlank) (i : Fin (n + 1)) : ((tm.repeatAtTime k T).trace 1 choice C).work (repeatTapeIdx l i) = parkedBlank

A nonfinal finish leaves banks after the next active bank parked.

theorem Complexity.NTM.trace_run_output {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) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.run j t q votes) (hout : C.output = parkedBlank) : ((tm.repeatAtTime k T).trace 1 choice C).output = parkedBlank

The real output tape remains parked and blank through a run step.

theorem Complexity.NTM.trace_rewind_output {n k T : ℕ} (tm : NTM n) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (j : Fin k) (r : Fin (T + 1)) (q : tm.Q) (votes : Fin k → Bool) (inputDone : Bool) (bankDone : Fin (n + 1) → Bool) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.rewind j r q votes inputDone bankDone) (hout : C.output = parkedBlank) : ((tm.repeatAtTime k T).trace 1 choice C).output = parkedBlank

The real output tape remains parked and blank through a rewind step.

theorem Complexity.NTM.trace_finish_output {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) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hout : C.output = parkedBlank) : ((tm.repeatAtTime k T).trace 1 choice C).output = parkedBlank

A nonfinal finish transition preserves the real output tape.

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

Run steps preserve the complete fresh-bank frame for the active trial.

theorem Complexity.NTM.RepeatFrame.rewind {n k T : ℕ} (tm : NTM n) {x : List Bool} {C : Cfg (k * (n + 1)) (tm.RepeatQ k T)} {j : Fin k} {r : Fin (T + 1)} {q : tm.Q} {votes : Fin k → Bool} {inputDone : Bool} {bankDone : Fin (n + 1) → Bool} (hframe : RepeatFrame x j C) (hstate : C.state = RepeatQ.rewind j r q votes inputDone bankDone) (choice : Fin 1 → Bool) : RepeatFrame x j ((tm.repeatAtTime k T).trace 1 choice C)

Rewind steps preserve the complete fresh-bank frame for the active trial.

theorem Complexity.NTM.RepeatFrame.finish {n k T : ℕ} (tm : NTM n) {x : List Bool} {C : Cfg (k * (n + 1)) (tm.RepeatQ k T)} {j : Fin k} {q : tm.Q} {votes : Fin k → Bool} (hframe : RepeatFrame x j C) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (choice : Fin 1 → Bool) : have j' := ⟨↑j + 1, hj⟩; RepeatFrame x j' ((tm.repeatAtTime k T).trace 1 choice C)

A nonfinal finish advances the frame boundary to the next trial.

theorem Complexity.NTM.trace_finish_next_input {n k T : ℕ} (tm : NTM n) (x : List Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hin : C.input = parkedInput x) : ((tm.repeatAtTime k T).trace 1 choice C).input = (tm.initCfg x).input

A nonfinal finish positions the input tape exactly at the source initial tape.

theorem Complexity.NTM.trace_finish_next_bank {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) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hbank : ∀ (i : Fin (n + 1)), C.work (repeatTapeIdx ⟨↑j + 1, hj⟩ i) = parkedBlank) (i : Fin (n + 1)) : ((tm.repeatAtTime k T).trace 1 choice C).work (repeatTapeIdx ⟨↑j + 1, hj⟩ i) = Tape.init []

A nonfinal finish positions every tape of the next fresh bank at its source initial blank tape.

theorem Complexity.NTM.trace_finish_next_project {n k T : ℕ} (tm : NTM n) (x : List Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hin : C.input = parkedInput x) (hbank : ∀ (i : Fin (n + 1)), C.work (repeatTapeIdx ⟨↑j + 1, hj⟩ i) = parkedBlank) : tm.repeatProjectCfg ⟨↑j + 1, hj⟩ tm.qstart ((tm.repeatAtTime k T).trace 1 choice C) = tm.initCfg x

The nonfinal finish handoff initializes the complete source projection for the next trial.

theorem Complexity.NTM.RepeatFrame.finish_next_project {n k T : ℕ} (tm : NTM n) {x : List Bool} {C : Cfg (k * (n + 1)) (tm.RepeatQ k T)} {j : Fin k} {q : tm.Q} {votes : Fin k → Bool} (hframe : RepeatFrame x j C) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hin : C.input = parkedInput x) (choice : Fin 1 → Bool) : tm.repeatProjectCfg ⟨↑j + 1, hj⟩ tm.qstart ((tm.repeatAtTime k T).trace 1 choice C) = tm.initCfg x

Once rewind has parked the input, a nonfinal finish starts the next trial at exactly the source initial configuration.