Setup boundary for fixed-time repetition

This internal module packages the complete two-transition setup as the base case of the repetition schedule. It also handles the degenerate zero-trial machine, whose setup immediately halts with the empty majority verdict.

Main results

• NTM.repeatAtTime_trace_setup_ready — all first-trial boundary ingredients
• NTM.repeatAtTime_trace_setup_boundary — the initial RepeatBoundary
• NTM.repeatAtTime_trace_zero_repetitions — the k = 0 endpoint

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

The second setup transition preserves the fresh-bank frame while positioning bank zero, uniformly for positive and zero simulation time.

theorem Complexity.NTM.repeatAtTime_trace_setup_ready {n k T : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (seed : Fin (k * T) → Bool) (choices : Fin 2 → Bool) : have j := ⟨0, hk⟩; have votes := fun (x : Fin k) => false; have C := (tm.repeatAtTime k T).trace 2 choices ((tm.repeatAtTime k T).initCfg x); tm.RepeatCompletedVotes x seed votes 0 ∧ C.state = tm.repeatTrialStartState j votes ∧ tm.repeatProjectCfg j tm.qstart C = tm.initCfg x ∧ C.input.StartInvariant ∧ (∀ (i : Fin (k * (n + 1))), (C.work i).StartInvariant) ∧ C.output.StartInvariant ∧ C.input.head = 0 ∧ (∀ (i : Fin (n + 1)), (C.work (repeatTapeIdx j i)).head = 0) ∧ RepeatFrame x j C ∧ RepeatOtherParked j C

With at least one trial, the full two-step setup establishes every fact needed to start the first trial and its outer-induction boundary.

theorem Complexity.NTM.repeatAtTime_trace_setup_boundary {n k T : ℕ} (tm : NTM n) (x : List Bool) (hk : 0 < k) (seed : Fin (k * T) → Bool) (choices : Fin 2 → Bool) : tm.RepeatBoundary x seed 0 ((tm.repeatAtTime k T).trace 2 choices ((tm.repeatAtTime k T).initCfg x))

The complete setup trace is the initial outer boundary before trial zero.

theorem Complexity.NTM.repeatAtTime_trace_zero_repetitions {n T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (0 * T) → Bool) (choices : Fin (repeatAtTimeSteps 0 T) → Bool) : have C := (tm.repeatAtTime 0 T).trace (repeatAtTimeSteps 0 T) choices ((tm.repeatAtTime 0 T).initCfg x); C.state = RepeatQ.halt ∧ C.output.head = 1 ∧ C.output.cells 1 = Γ.zero ∧ C.output.cells 1 = Γ.ofBool (majority (tm.repeatVotes x 0 T seed))

With no trials, the two setup transitions halt and write the strict majority of the empty vote vector, namely zero, to output cell one.