Setup and finish phases for fixed-time repetition

Correctness lemmas for the zero-time setup path and the final majority-writing transition of NTM.repeatAtTime.

theorem Complexity.NTM.repeatAtTime_begin_zero_simulates {n k : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (choice : Fin 1 → Bool) : have j := ⟨0, hk⟩; have votes := fun (x : Fin k) => false; have C := (tm.repeatAtTime k 0).trace 1 choice (tm.repeatParkedCfg k 0 x); (C.state = RepeatQ.rewind j ⟨0, ⋯⟩ tm.qstart votes false fun (x : Fin (n + 1)) => false) ∧ tm.repeatProjectCfg j tm.qstart C = tm.initCfg x ∧ C.input.StartInvariant ∧ (∀ (i : Fin (k * (n + 1))), (C.work i).StartInvariant) ∧ C.output.StartInvariant ∧ (∀ (i : Fin (k * (n + 1))), (repeatTapeCoord i).1 ≠ j → C.work i = (Tape.init []).move Dir3.right) ∧ C.output = (Tape.init []).move Dir3.right

For T = 0, the second setup transition enters rewind immediately. Trial zero is the exact source initial configuration, inactive banks and the real output remain parked, and all tape start invariants hold.

theorem Complexity.NTM.repeatAtTime_trace_finish_last {n k T : ℕ} (tm : NTM n) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (c : Cfg n tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hlast : ¬↑j + 1 < k) (hsim : tm.RepeatSimulates j q c C) (hactiveHead : (C.work (repeatOutputIdx j)).head = 1) (hout : C.output.StartInvariant) (houtHead : C.output.head = 1) : have accepted := decide (c.state = tm.qhalt ∧ c.output.cells 1 = Γ.one); have verdict := majority (Function.update votes j accepted); have C' := (tm.repeatAtTime k T).trace 1 choice C; C'.state = RepeatQ.halt ∧ C'.output.head = 1 ∧ C'.output.cells 1 = Γ.ofBool verdict

On the last repetition, one .finish transition records the current trial's source verdict, halts the wrapper, and writes the strict majority to real output cell one.