Schedule arithmetic internals for fixed-time repetition

This module proves the arithmetic and compact-seed alignment facts shared by the public repetition surface and the proof-internal schedule. Keeping these proofs below the public surface prevents internal correctness modules from depending on Complexitylib.Models.TuringMachine.Repetition.

Exact schedule arithmetic

theorem Complexity.NTM.repeatAtTimeStride_zero_internal : repeatAtTimeStride 0 = 2

Internal form of the zero-time stride calculation.

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

Internal form of the successor-time stride calculation.

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

Internal form of the zero-repetition schedule calculation.

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

Internal form of the zero-time schedule calculation.

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

Internal form of the successor-repetition schedule calculation.

Compact-seed alignment

theorem Complexity.NTM.repeatRandomSeed_apply_repeatChoiceIdx_internal (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)

Internal form of the compact-seed and machine-schedule alignment.