Fixed-time probabilistic-machine repetition

This public surface records the exact arithmetic schedule of NTM.repeatAtTime and connects its simulated-step positions to the generic compact-seed projection from Complexitylib.Classes.FiniteCounting.

It deliberately makes no trace or acceptance claim: those require the simulation invariants proved in the internal correctness layer.

Main results

• NTM.repeatAtTimeStride_zero, NTM.repeatAtTimeStride_succ — stride arithmetic
• NTM.repeatAtTimeSteps_zero, NTM.repeatAtTimeSteps_succ — total-time arithmetic
• NTM.repeatRandomSeed_apply_repeatChoiceIdx — compact and machine schedules align

Exact schedule arithmetic

@[simp]

theorem Complexity.NTM.repeatAtTimeStride_zero : repeatAtTimeStride 0 = 2

With zero simulated steps, a stride consists only of rewind and finish.

theorem Complexity.NTM.repeatAtTimeStride_succ (T : ℕ) : repeatAtTimeStride (T + 1) = repeatAtTimeStride T + 2

Increasing the simulated time by one adds one simulation transition and one rewind transition to every stride.

@[simp]

theorem Complexity.NTM.repeatAtTimeSteps_zero (T : ℕ) : repeatAtTimeSteps 0 T = 2

Zero repetitions use exactly the two leading administrative transitions.

@[simp]

theorem Complexity.NTM.repeatAtTimeSteps_zero_time (k : ℕ) : repeatAtTimeSteps k 0 = 2 + k * 2

At zero simulated time, every repetition contributes its two administrative transitions.

theorem Complexity.NTM.repeatAtTimeSteps_succ (k T : ℕ) : repeatAtTimeSteps (k + 1) T = repeatAtTimeSteps k T + repeatAtTimeStride T

Adding one repetition appends exactly one stride.

Compact-seed alignment

@[simp]

theorem Complexity.NTM.repeatRandomSeed_apply_repeatChoiceIdx (k T : ℕ) (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (t : Fin T) : repeatRandomSeed k T choices (finProdFinEquiv (j, t)) = choices (repeatChoiceIdx T j t)

The generic compact repetition seed selects exactly the global choice position used by repeatAtTime for simulated step t of repetition j.