Finish-step vote semantics for fixed-time repetition

This module identifies the bit recorded by a repetition finish transition with the corresponding source-machine trial verdict. It combines that control-state step with the fresh-bank frame layer to hand the outer induction an exact next source configuration, and specializes the final finish theorem to repeatVotes.

Main results

• NTM.repeatTrialVote_eq_decide_trace — source trace predicate for one trial
• NTM.repeatAtTime_trace_finish_next_vote — exact nonfinal control-state update
• NTM.repeatAtTime_trace_finish_next — control, projection, and frame handoff
• NTM.repeatAtTime_trace_finish_last_votes — final majority in source-vote form

theorem Complexity.NTM.repeatTrialVote_eq_decide_trace {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (j : Fin k) : tm.repeatTrialVote x k T seed j = decide (have c := tm.trace T ((blocksEquiv k T) seed j) (tm.initCfg x); c.state = tm.qhalt ∧ c.output.cells 1 = Γ.one)

A compact-seed trial vote is exactly the halted-with-one predicate of the corresponding T-step source trace.

theorem Complexity.NTM.repeatFinishAccepted_eq_repeatVotes {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (j : Fin k) (q : tm.Q) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (hsim : tm.RepeatSimulates j q (tm.trace T ((blocksEquiv k T) seed j) (tm.initCfg x)) C) (hactiveHead : (C.work (repeatOutputIdx j)).head = 1) : decide (q = tm.qhalt ∧ (C.work (repeatOutputIdx j)).read = Γ.one) = tm.repeatVotes x k T seed j

The accepting bit computed by .finish agrees with the corresponding entry of the source-machine vote vector.

theorem Complexity.NTM.repeatAtTime_trace_finish_next_vote {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hsim : tm.RepeatSimulates j q (tm.trace T ((blocksEquiv k T) seed j) (tm.initCfg x)) C) (hactiveHead : (C.work (repeatOutputIdx j)).head = 1) : have j' := ⟨↑j + 1, hj⟩; have votes' := Function.update votes j (tm.repeatVotes x k T seed j); have C' := (tm.repeatAtTime k T).trace 1 choice C; C'.state = if hT : 0 < T then RepeatQ.run j' ⟨0, hT⟩ tm.qstart votes' else RepeatQ.rewind j' ⟨0, ⋯⟩ tm.qstart votes' false fun (x : Fin (n + 1)) => false

A nonfinal finish transition records the exact source trial vote and enters the next trial's run state, or its rewind state when T = 0.

theorem Complexity.NTM.repeatAtTime_trace_finish_next {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hj : ↑j + 1 < k) (hsim : tm.RepeatSimulates j q (tm.trace T ((blocksEquiv k T) seed j) (tm.initCfg x)) C) (hactiveHead : (C.work (repeatOutputIdx j)).head = 1) (hframe : RepeatFrame x j C) (hin : C.input = parkedInput x) : have j' := ⟨↑j + 1, hj⟩; have votes' := Function.update votes j (tm.repeatVotes x k T seed j); have C' := (tm.repeatAtTime k T).trace 1 choice C; (C'.state = if hT : 0 < T then RepeatQ.run j' ⟨0, hT⟩ tm.qstart votes' else RepeatQ.rewind j' ⟨0, ⋯⟩ tm.qstart votes' false fun (x : Fin (n + 1)) => false) ∧ tm.repeatProjectCfg j' tm.qstart C' = tm.initCfg x ∧ RepeatFrame x j' C'

A nonfinal finish simultaneously records the source vote, initializes the next source projection, and advances the fresh-bank frame.

theorem Complexity.NTM.repeatAtTime_trace_finish_last_votes {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (j : Fin k) (q : tm.Q) (votes : Fin k → Bool) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) (choice : Fin 1 → Bool) (hstate : C.state = RepeatQ.finish j q votes) (hlast : ¬↑j + 1 < k) (hsim : tm.RepeatSimulates j q (tm.trace T ((blocksEquiv k T) seed j) (tm.initCfg x)) C) (hactiveHead : (C.work (repeatOutputIdx j)).head = 1) (hframe : RepeatFrame x j C) : have C' := (tm.repeatAtTime k T).trace 1 choice C; C'.state = RepeatQ.halt ∧ C'.output.head = 1 ∧ C'.output.cells 1 = Γ.ofBool (majority (Function.update votes j (tm.repeatVotes x k T seed j)))

On the last trial, the wrapper writes the strict majority of the source trial-vote vector with the current trial updated at j.