Correctness and amplification for fixed-time repetition

This public surface proves that NTM.repeatAtTime halts at its advertised schedule and returns the strict majority of k independent source trials. It then cancels the wrapper's administrative random bits to obtain an exact acceptance-probability identity and the standard bounded-error amplification bounds for 12s + 1 trials.

The source machine need only halt on every T-step path for the fixed input.

Main results

• NTM.repeatAtTime_trace_correct — pathwise fixed-schedule correctness
• NTM.repeatAtTime_acceptProb_eq_eventProb — exact majority-event probability
• NTM.repeatAtTime_acceptProb_zero_repetitions — unconditional zero-trial behavior
• NTM.repeatAtTime_acceptProb_ge_one_sub_two_pow — yes-instance amplification
• NTM.repeatAtTime_acceptProb_le_two_pow — no-instance amplification

theorem Complexity.NTM.acceptProb_eq_eventProb_repeatAcceptEvent {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : tm.acceptProb x T = eventProb (tm.repeatAcceptEvent x T)

The source acceptance probability is the event probability of the single-trial accepting choice set used by the repetition construction.

@[simp]

theorem Complexity.NTM.repeatAtTime_acceptProb_zero_repetitions {n : ℕ} (tm : NTM n) (x : List Bool) (T : ℕ) : (tm.repeatAtTime 0 T).acceptProb x 2 = 0

With no trials, the repetition wrapper rejects unconditionally. This degenerate case does not require the source machine to halt.

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

Pathwise correctness of fixed-time repetition. If every source path has halted after T steps, the repeated machine halts at its exact advertised time and writes the majority of the k source-trial verdicts selected by its compact simulation seed.

theorem Complexity.NTM.repeatAtTime_acceptProb_eq_eventProb {n : ℕ} (tm : NTM n) (x : List Bool) (k T : ℕ) (hhalts : ∀ (runChoices : Fin T → Bool), tm.halted (tm.trace T runChoices (tm.initCfg x))) : (tm.repeatAtTime k T).acceptProb x (repeatAtTimeSteps k T) = eventProb {seed : Fin (k * T) → Bool | blockMajority (tm.repeatAcceptEvent x T) seed = true}

The repeated machine's acceptance probability is exactly the probability that a strict majority of its compact k source-choice blocks accept. Random choices consumed by setup, rewind, and finish transitions cancel completely.

theorem Complexity.NTM.repeatAtTime_acceptProb_ge_one_sub_two_pow {n : ℕ} (tm : NTM n) (x : List Bool) (T s : ℕ) (hhalts : ∀ (runChoices : Fin T → Bool), tm.halted (tm.trace T runChoices (tm.initCfg x))) (haccept : 2 / 3 ≤ tm.acceptProb x T) : 1 - 1 / 2 ^ s ≤ (tm.repeatAtTime (12 * s + 1) T).acceptProb x (repeatAtTimeSteps (12 * s + 1) T)

Yes-instance amplification. A source acceptance probability at least 2/3 becomes at least 1 - 2⁻s after 12s + 1 independent trials.

theorem Complexity.NTM.repeatAtTime_acceptProb_le_two_pow {n : ℕ} (tm : NTM n) (x : List Bool) (T s : ℕ) (hhalts : ∀ (runChoices : Fin T → Bool), tm.halted (tm.trace T runChoices (tm.initCfg x))) (haccept : tm.acceptProb x T ≤ 1 / 3) : (tm.repeatAtTime (12 * s + 1) T).acceptProb x (repeatAtTimeSteps (12 * s + 1) T) ≤ 1 / 2 ^ s

No-instance amplification. A source acceptance probability at most 1/3 becomes at most 2⁻s after 12s + 1 independent trials.