Correctness internals for fixed-time repetition

This file proves the local simulation and fixed-rewind invariants used by the public correctness theorems for NTM.repeatAtTime.

def Complexity.NTM.repeatProjectCfg {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : Cfg n tm.Q

Project one active repetition bank back to a source-machine configuration. The source state is carried in the repetition control and is therefore supplied separately.

Equations

• tm.repeatProjectCfg j q C = { state := q, input := C.input, work := fun (i : Fin n) => C.work (Complexity.NTM.repeatWorkIdx j i), output := C.work (Complexity.NTM.repeatOutputIdx j) }

def Complexity.NTM.repeatSourceStep {n : ℕ} (tm : NTM n) (b : Bool) (c : Cfg n tm.Q) : Cfg n tm.Q

Apply one source transition without a halting check. Repetition uses this operation exactly in non-halted .run states.

Equations

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

theorem Complexity.NTM.trace_one_eq_repeatSourceStep {n : ℕ} (tm : NTM n) (b : Bool) (c : Cfg n tm.Q) (h : c.state ≠ tm.qhalt) : tm.trace 1 (fun (x : Fin 1) => b) c = tm.repeatSourceStep b c

On a non-halted configuration, a one-slot trace is the raw source step.

def Complexity.NTM.RepeatSimulates {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (c : Cfg n tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : Prop

An active repetition bank simulates c. Before source halting its complete projection agrees with c; after halting only the state and tape cells are required to agree, because fixed-slot padding may bounce a head off cell zero.

Equations

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

theorem Complexity.NTM.RepeatSimulates.of_project_eq {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (c : Cfg n tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (h : tm.repeatProjectCfg j q C = c) : tm.RepeatSimulates j q c C

Exact projection implies the simulation relation.

theorem Complexity.NTM.repeatSafeDir_eq (head : Γ) (dir : Dir3) (h : head = Γ.start → dir = Dir3.right) : repeatSafeDir head dir = dir

On a transition direction already satisfying the model's left-end rule, the repetition machine's defensive direction guard is inert.

theorem Complexity.NTM.repeatPositionTape_eq (t : Tape) (hread : t.read ≠ Γ.start) : t.writeAndMove (TM.readBackWrite t.read).toΓ (repeatSafeDir t.read (TM.moveLeftDir t.read)) = t.move Dir3.left

Positioning an off-start tape writes its current symbol back and moves its head one cell left.

theorem Complexity.NTM.repeatPositionInput_init (x : List Bool) : have t := (Tape.init (List.map Γ.ofBool x)).move Dir3.right; t.writeAndMove (TM.readBackWrite t.read).toΓ (repeatSafeDir t.read (TM.moveLeftDir t.read)) = Tape.init (List.map Γ.ofBool x)

A parked initialized input returns to its initial head position under the positioning action.

theorem Complexity.NTM.repeatPositionBlank_init : have t := (Tape.init []).move Dir3.right; t.writeAndMove (TM.readBackWrite t.read).toΓ (repeatSafeDir t.read (TM.moveLeftDir t.read)) = Tape.init []

A parked blank work tape returns to its initial head position under the positioning action.

Fixed-time rewind of one tape

def Complexity.NTM.repeatFixedRewindTapeStep (s : Tape × Bool) : Tape × Bool

The one-tape component of a repetition rewind transition.

Equations

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

def Complexity.NTM.repeatFixedRewindTapeIter : ℕ → Tape × Bool → Tape × Bool

Iterate the one-tape rewind component in the cons-first order of NTM.trace.

Equations

• Complexity.NTM.repeatFixedRewindTapeIter 0 x✝ = x✝
• Complexity.NTM.repeatFixedRewindTapeIter m.succ x✝ = Complexity.NTM.repeatFixedRewindTapeIter m (Complexity.NTM.repeatFixedRewindTapeStep x✝)

theorem Complexity.NTM.repeatStartInvariant_read_eq_start_iff (t : Tape) (h : t.StartInvariant) : t.read = Γ.start ↔ t.head = 0

Under the unique-left-marker invariant, a tape reads ▷ exactly at cell zero.

theorem Complexity.NTM.repeatFixedRewindTapeIter_bound (T : ℕ) (t : Tape) (h : t.StartInvariant) (hh : t.head ≤ T) : have s := repeatFixedRewindTapeIter (T + 1) (t, false); s.2 = true ∧ s.1.head = 1 ∧ s.1.cells = t.cells

T + 1 fixed rewind steps park any invariant tape whose head is at most T at cell one, set its completion flag, and preserve all cells.

def Complexity.NTM.repeatParkedCfg {n : ℕ} (tm : NTM n) (k T : ℕ) (x : List Bool) : Cfg (k * (n + 1)) (tm.RepeatQ k T)

Configuration after the first setup transition: all tapes are parked at cell one and the control is ready to choose the first repetition.

Equations

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

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

The first setup transition parks every tape at cell one.

theorem Complexity.NTM.repeatAtTime_begin_simulates {n k T : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (hT : 0 < T) (choice : Fin 1 → Bool) : have j := ⟨0, hk⟩; have t := ⟨0, hT⟩; have votes := fun (x : Fin k) => false; have C := (tm.repeatAtTime k T).trace 1 choice (tm.repeatParkedCfg k T x); C.state = RepeatQ.run j t tm.qstart votes ∧ tm.RepeatSimulates j tm.qstart (tm.initCfg x) C

With at least one repetition and one simulated step, the second setup transition positions trial zero exactly at the source initial configuration.

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

With positive repetition count and simulation time, the second setup transition gives trial zero the exact source initial configuration. This stronger projection fact also covers tm.qstart = tm.qhalt.

theorem Complexity.NTM.repeatAtTime_trace_setup_simulates {n k T : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (hT : 0 < T) (choices : Fin 2 → Bool) : have j := ⟨0, hk⟩; have t := ⟨0, hT⟩; have votes := fun (x : Fin k) => false; have C := (tm.repeatAtTime k T).trace 2 choices ((tm.repeatAtTime k T).initCfg x); C.state = RepeatQ.run j t tm.qstart votes ∧ tm.RepeatSimulates j tm.qstart (tm.initCfg x) C

The complete two-transition setup establishes the source initial configuration in trial zero.

theorem Complexity.NTM.repeatAtTime_trace_setup_project {n k T : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (hT : 0 < T) (choices : Fin 2 → Bool) : have j := ⟨0, hk⟩; have C := (tm.repeatAtTime k T).trace 2 choices ((tm.repeatAtTime k T).initCfg x); tm.repeatProjectCfg j tm.qstart C = tm.initCfg x

The complete positive-time setup gives trial zero the exact source initial configuration.

theorem Complexity.NTM.repeatAtTime_run_project {n k T : ℕ} (tm : NTM n) (j : Fin k) (t : Fin T) (q : tm.Q) (votes : Fin k → Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (b : Bool) (hstate : C.state = RepeatQ.run j t q votes) (hq : q ≠ tm.qhalt) : have c := tm.repeatProjectCfg j q C; have c' := tm.repeatSourceStep b c; have C' := (tm.repeatAtTime k T).trace 1 (fun (x : Fin 1) => b) C; C'.state = tm.repeatAfterRunState j t c'.state votes ∧ tm.repeatProjectCfg j c'.state C' = c'

One non-halted repetition .run transition commutes exactly with one raw source transition through the active-bank projection.

theorem Complexity.NTM.repeatAtTime_run_project_trace {n k T : ℕ} (tm : NTM n) (j : Fin k) (t : Fin T) (q : tm.Q) (votes : Fin k → Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (b : Bool) (hstate : C.state = RepeatQ.run j t q votes) (hq : q ≠ tm.qhalt) : have c := tm.repeatProjectCfg j q C; have c' := tm.trace 1 (fun (x : Fin 1) => b) c; have C' := (tm.repeatAtTime k T).trace 1 (fun (x : Fin 1) => b) C; C'.state = tm.repeatAfterRunState j t c'.state votes ∧ tm.repeatProjectCfg j c'.state C' = c'

One non-halted repetition .run transition projects to the source machine's one-step trace, including the source's own halting semantics.

theorem Complexity.NTM.repeatAtTime_run_padding_simulates {n k T : ℕ} (tm : NTM n) (j : Fin k) (t : Fin T) (q : tm.Q) (votes : Fin k → Bool) (c : Cfg n tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (b : Bool) (hstate : C.state = RepeatQ.run j t q votes) (hq : q = tm.qhalt) (hsim : tm.RepeatSimulates j q c C) (hinv : ∀ (i : Fin (k * (n + 1))), (C.work i).StartInvariant) : have C' := (tm.repeatAtTime k T).trace 1 (fun (x : Fin 1) => b) C; C'.state = tm.repeatAfterRunState j t q votes ∧ tm.RepeatSimulates j q c C'

A .run slot after the source has halted advances the fixed counter while preserving the source state and every projected tape cell. Thus the halt-aware simulation relation survives padding slots.

A complete fixed-width simulation run

theorem Complexity.NTM.repeatAtTime_trace_run_prefix {n k T : ℕ} (tm : NTM n) (hT : 0 < T) (j : Fin k) (votes : Fin k → Bool) (g : ℕ → 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) (m : ℕ) (hm : m < T) : have c := tm.trace m (fun (i : Fin m) => g ↑i) c₀; have C := (tm.repeatAtTime k T).trace m (fun (i : Fin m) => g ↑i) C₀; C.state = RepeatQ.run j ⟨m, hm⟩ c.state votes ∧ tm.RepeatSimulates j c.state c C ∧ C.input.StartInvariant ∧ (∀ (i : Fin (k * (n + 1))), (C.work i).StartInvariant) ∧ C.output.StartInvariant

Every proper prefix of a fixed-width simulation run remains in .run, tracks the corresponding source prefix, and preserves all start invariants.

theorem Complexity.NTM.repeatAtTime_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) : have c := tm.trace T choices c₀; have C := (tm.repeatAtTime k T).trace T choices C₀; (C.state = RepeatQ.rewind j ⟨0, ⋯⟩ c.state votes false fun (x : Fin (n + 1)) => false) ∧ tm.RepeatSimulates j c.state c C ∧ C.input.StartInvariant ∧ (∀ (i : Fin (k * (n + 1))), (C.work i).StartInvariant) ∧ C.output.StartInvariant

Exactly T simulation slots advance trial j from its initial .run state to rewind counter zero. The active bank agrees with the source T-step trace even when the source halts early, and all tape start invariants persist.