Pathwise correctness of fixed-time repetition

This module performs the outer induction over the exact repetition schedule. When every T-choice source trace on the fixed input halts, each wrapper trial records the corresponding compact-seed vote, transfers the fresh-bank boundary, and the final trial writes their strict majority.

Main results

• NTM.repeatAtTime_outer_correct — every exact trial boundary is correct
• NTM.repeatAtTime_trace_correct_internal — final full-trace majority theorem

theorem Complexity.NTM.repeatAtTime_outer_correct {n k T : ℕ} (tm : NTM n) (x : List Bool) (choices : Fin (repeatAtTimeSteps k T) → Bool) (hhalt : ∀ (runChoices : Fin T → Bool), (tm.trace T runChoices (tm.initCfg x)).state = tm.qhalt) : tm.RepeatOuterClaim x choices

Under fixed-input all-paths halting at time T, every exact wrapper trial boundary satisfies RepeatBoundary.

theorem Complexity.NTM.repeatAtTime_trace_correct_internal {n k T : ℕ} (tm : NTM n) (x : List Bool) (choices : Fin (repeatAtTimeSteps k T) → Bool) (hhalt : ∀ (runChoices : Fin T → Bool), (tm.trace T runChoices (tm.initCfg x)).state = tm.qhalt) : have C := (tm.repeatAtTime k T).trace (repeatAtTimeSteps k T) choices ((tm.repeatAtTime k T).initCfg x); C.state = RepeatQ.halt ∧ C.output.head = 1 ∧ C.output.cells 1 = Γ.ofBool (blockMajority (tm.repeatAcceptEvent x T) (repeatRandomSeed k T choices))

Final pathwise correctness: the full wrapper trace halts and writes the strict majority of the source accepting-event blocks selected by the compact simulation seed.