Vote bookkeeping for fixed-time repetition

This file connects the finite-control vote vector of NTM.repeatAtTime to the block-event majority API and provides the update invariant used by the outer trial induction.

def Complexity.NTM.repeatTrialVote {n : ℕ} (tm : NTM n) (x : List Bool) (k T : ℕ) (seed : Fin (k * T) → Bool) (j : Fin k) : Bool

Verdict of source trial j in a compact k * T repetition seed.

Equations

• tm.repeatTrialVote x k T seed j = decide ((Complexity.blocksEquiv k T) seed j ∈ tm.repeatAcceptEvent x T)

def Complexity.NTM.repeatVotes {n : ℕ} (tm : NTM n) (x : List Bool) (k T : ℕ) (seed : Fin (k * T) → Bool) : Fin k → Bool

The vector of all source-trial verdicts in a compact repetition seed.

Equations

• tm.repeatVotes x k T seed j = tm.repeatTrialVote x k T seed j

@[simp]

theorem Complexity.NTM.repeatTrialVote_eq_true_iff {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (j : Fin k) : tm.repeatTrialVote x k T seed j = true ↔ (blocksEquiv k T) seed j ∈ tm.repeatAcceptEvent x T

theorem Complexity.NTM.popCount_repeatVotes {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) : popCount (tm.repeatVotes x k T seed) = blockEventCount (tm.repeatAcceptEvent x T) seed

Counting true machine votes is the generic block-event count.

theorem Complexity.NTM.majority_repeatVotes {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) : majority (tm.repeatVotes x k T seed) = blockMajority (tm.repeatAcceptEvent x T) seed

The strict majority of the machine's vote vector is exactly the generic block majority of the source accepting event.

def Complexity.NTM.RepeatVotesThrough {k : ℕ} (expected votes : Fin k → Bool) (m : ℕ) : Prop

votes contains the expected verdicts below m and false in every not-yet-completed trial slot.

Equations

• Complexity.NTM.RepeatVotesThrough expected votes m = ∀ (i : Fin k), votes i = if ↑i < m then expected i else false

theorem Complexity.NTM.RepeatVotesThrough.zero {k : ℕ} (expected : Fin k → Bool) : RepeatVotesThrough expected (fun (x : Fin k) => false) 0

theorem Complexity.NTM.RepeatVotesThrough.update {k : ℕ} {expected votes : Fin k → Bool} {m : ℕ} (hm : m < k) (h : RepeatVotesThrough expected votes m) : RepeatVotesThrough expected (Function.update votes ⟨m, hm⟩ (expected ⟨m, hm⟩)) (m + 1)

Recording trial m advances the vote invariant by one slot.

theorem Complexity.NTM.RepeatVotesThrough.eq_expected {k : ℕ} {expected votes : Fin k → Bool} (h : RepeatVotesThrough expected votes k) : votes = expected

Once all k trials are recorded, the finite-control vector is the full expected vote vector.