Complete trials for fixed-time repetition

This internal module composes one fixed-width source simulation with the administrative rewind. It handles both positive simulation widths and the zero-time path, and packages the finish-state facts needed by the vote step.

Main results

• NTM.RepeatTrialComplete — finish-state simulation, parking, and frame facts
• NTM.repeatAtTime_trace_rewind_trial — common rewind-to-finish composition
• NTM.repeatAtTime_trace_trial_pos — a complete positive-time trial
• NTM.repeatAtTime_trace_trial_zero — a complete zero-time trial
• NTM.repeatAtTime_trace_trial — the combined trial theorem for every T

def Complexity.NTM.RepeatTrialComplete {n k T : ℕ} (tm : NTM n) (x : List Bool) (j : Fin k) (votes : Fin k → Bool) (c : Cfg n tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : Prop

Facts established when one repetition trial has completed its fixed rewind and reached .finish.

Equations

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

theorem Complexity.NTM.RepeatFrame.trace_run_prefix {n k T : ℕ} (tm : NTM n) (hT : 0 < T) (x : List Bool) (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) (hframe : RepeatFrame x j C₀) (m : ℕ) (hm : m < T) : RepeatFrame x j ((tm.repeatAtTime k T).trace m (fun (i : Fin m) => g ↑i) C₀)

Every proper prefix of a positive-time run preserves the fresh-bank frame.

theorem Complexity.NTM.RepeatFrame.trace_run {n k T : ℕ} (tm : NTM n) (hT : 0 < T) (x : List Bool) (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) (hframe : RepeatFrame x j C₀) : RepeatFrame x j ((tm.repeatAtTime k T).trace T choices C₀)

A complete positive-time run preserves the fresh-bank frame.

theorem Complexity.NTM.repeatAtTime_trace_rewind_trial {n k T : ℕ} (tm : NTM n) (x : List Bool) (j : Fin k) (votes : Fin k → Bool) (c : Cfg n tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hstate : C.state = RepeatQ.rewind j ⟨0, ⋯⟩ c.state votes false fun (x : Fin (n + 1)) => false) (hsim : tm.RepeatSimulates j c.state c C) (hhalt : c.state = tm.qhalt) (hinp : C.input.StartInvariant) (hwork : ∀ (i : Fin (k * (n + 1))), (C.work i).StartInvariant) (hout : C.output.StartInvariant) (hinputHead : C.input.head ≤ T) (hactiveHead : ∀ (i : Fin (n + 1)), (C.work (repeatTapeIdx j i)).head ≤ T) (hframe : RepeatFrame x j C) (hparked : RepeatOtherParked j C) (choices : Fin (T + 1) → Bool) : tm.RepeatTrialComplete x j votes c ((tm.repeatAtTime k T).trace (T + 1) choices C)

Fixed rewind turns a halted source simulation into the complete trial facts consumed by a finish transition.

theorem Complexity.NTM.repeatAtTime_trace_trial_pos {n k T : ℕ} (tm : NTM n) (x : List Bool) (hT : 0 < T) (j : Fin k) (votes : Fin k → Bool) (runChoices : Fin T → Bool) (rewindChoices : Fin (T + 1) → Bool) (C₀ : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hstate : C₀.state = RepeatQ.run j ⟨0, hT⟩ tm.qstart votes) (hproject : tm.repeatProjectCfg j tm.qstart C₀ = tm.initCfg x) (hinp : C₀.input.StartInvariant) (hwork : ∀ (i : Fin (k * (n + 1))), (C₀.work i).StartInvariant) (hout : C₀.output.StartInvariant) (hinputHead : C₀.input.head = 0) (hactiveHead : ∀ (i : Fin (n + 1)), (C₀.work (repeatTapeIdx j i)).head = 0) (hframe : RepeatFrame x j C₀) (hparked : RepeatOtherParked j C₀) (hhalt : (tm.trace T runChoices (tm.initCfg x)).state = tm.qhalt) : tm.RepeatTrialComplete x j votes (tm.trace T runChoices (tm.initCfg x)) ((tm.repeatAtTime k T).trace (T + 1) rewindChoices ((tm.repeatAtTime k T).trace T runChoices C₀))

One positive-time trial simulates exactly T source steps and then rewinds to a complete finish configuration.

theorem Complexity.NTM.repeatAtTime_trace_trial_zero {n k : ℕ} (tm : NTM n) (x : List Bool) (j : Fin k) (votes : Fin k → Bool) (rewindChoices : Fin 1 → Bool) (C₀ : Cfg (k * (n + 1)) (tm.RepeatQ k 0)) (hstate : C₀.state = RepeatQ.rewind j ⟨0, repeatAtTime_trace_trial_zero._proof_2⟩ tm.qstart votes false fun (x : Fin (n + 1)) => false) (hproject : tm.repeatProjectCfg j tm.qstart C₀ = tm.initCfg x) (hinp : C₀.input.StartInvariant) (hwork : ∀ (i : Fin (k * (n + 1))), (C₀.work i).StartInvariant) (hout : C₀.output.StartInvariant) (hinputHead : C₀.input.head = 0) (hactiveHead : ∀ (i : Fin (n + 1)), (C₀.work (repeatTapeIdx j i)).head = 0) (hframe : RepeatFrame x j C₀) (hparked : RepeatOtherParked j C₀) (hhalt : tm.qstart = tm.qhalt) : tm.RepeatTrialComplete x j votes (tm.initCfg x) ((tm.repeatAtTime k 0).trace 1 rewindChoices C₀)

A zero-time trial starts directly in rewind and reaches the same complete finish configuration as a positive-time trial.

theorem Complexity.NTM.repeatAtTime_trace_trial {n k T : ℕ} (tm : NTM n) (x : List Bool) (j : Fin k) (votes : Fin k → Bool) (runChoices : Fin T → Bool) (rewindChoices : Fin (T + 1) → Bool) (C₀ : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hstate : C₀.state = if hT : 0 < T then RepeatQ.run j ⟨0, hT⟩ tm.qstart votes else RepeatQ.rewind j ⟨0, ⋯⟩ tm.qstart votes false fun (x : Fin (n + 1)) => false) (hproject : tm.repeatProjectCfg j tm.qstart C₀ = tm.initCfg x) (hinp : C₀.input.StartInvariant) (hwork : ∀ (i : Fin (k * (n + 1))), (C₀.work i).StartInvariant) (hout : C₀.output.StartInvariant) (hinputHead : C₀.input.head = 0) (hactiveHead : ∀ (i : Fin (n + 1)), (C₀.work (repeatTapeIdx j i)).head = 0) (hframe : RepeatFrame x j C₀) (hparked : RepeatOtherParked j C₀) (hhalt : (tm.trace T runChoices (tm.initCfg x)).state = tm.qhalt) : tm.RepeatTrialComplete x j votes (tm.trace T runChoices (tm.initCfg x)) ((tm.repeatAtTime k T).trace (T + 1) rewindChoices ((tm.repeatAtTime k T).trace T runChoices C₀))

A complete trial theorem uniform in the simulation width: positive widths run the source for T slots before rewind, while width zero starts in rewind.