Outer schedule and boundary assertions for fixed-time repetition

This internal module splits the full wrapper choice string into the two setup choices and per-trial simulation and administrative slices. It also packages the completed-vote invariant and states the exact trial-boundary assertion used by the outer correctness induction.

The actual outer induction is deliberately separate: this file supplies its index algebra, choice slices, vote bookkeeping, and target predicate.

Main results

• NTM.repeatSetupChoices, repeatSimulationChoices, repeatAdminChoices — exact choice slices
• NTM.repeatSimulationChoices_eq_block — compact-seed alignment
• NTM.RepeatCompletedVotes — completed vote-prefix invariant
• NTM.RepeatBoundary, RepeatOuterClaim — outer-induction specification

Exact full-seed slices

def Complexity.NTM.repeatSetupChoiceIdx (k T : ℕ) (a : Fin 2) : Fin (repeatAtTimeSteps k T)

Global position of setup choice a.

Equations

• Complexity.NTM.repeatSetupChoiceIdx k T a = finSumFinEquiv (Sum.inl a)

def Complexity.NTM.repeatStrideChoiceIdx {k : ℕ} (T : ℕ) (j : Fin k) (s : Fin (repeatAtTimeStride T)) : Fin (repeatAtTimeSteps k T)

Global position of offset s in trial stride j.

Equations

• Complexity.NTM.repeatStrideChoiceIdx T j s = finSumFinEquiv (Sum.inr (finProdFinEquiv (j, s)))

def Complexity.NTM.repeatSimulationOffset (T : ℕ) (t : Fin T) : Fin (repeatAtTimeStride T)

Embed a simulation offset into the beginning of a trial stride.

Equations

• Complexity.NTM.repeatSimulationOffset T t = ⟨↑t, ⋯⟩

def Complexity.NTM.repeatAdminOffset (T : ℕ) (a : Fin (T + 2)) : Fin (repeatAtTimeStride T)

Embed an administrative offset after the T simulation choices.

Equations

• Complexity.NTM.repeatAdminOffset T a = ⟨T + ↑a, ⋯⟩

def Complexity.NTM.repeatSetupChoices {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) : Fin 2 → Bool

The two leading setup choices of a full repetition seed.

Equations

• Complexity.NTM.repeatSetupChoices choices a = choices (Complexity.NTM.repeatSetupChoiceIdx k T a)

def Complexity.NTM.repeatStrideChoices {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : Fin (repeatAtTimeStride T) → Bool

All choices in trial stride j.

Equations

• Complexity.NTM.repeatStrideChoices choices j s = choices (Complexity.NTM.repeatStrideChoiceIdx T j s)

def Complexity.NTM.repeatSimulationChoices {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : Fin T → Bool

The T source-simulation choices in trial j.

Equations

• Complexity.NTM.repeatSimulationChoices choices j t = Complexity.NTM.repeatStrideChoices choices j (Complexity.NTM.repeatSimulationOffset T t)

def Complexity.NTM.repeatAdminChoices {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : Fin (T + 2) → Bool

The T + 2 rewind-and-finish choices in trial j.

Equations

• Complexity.NTM.repeatAdminChoices choices j a = Complexity.NTM.repeatStrideChoices choices j (Complexity.NTM.repeatAdminOffset T a)

@[simp]

theorem Complexity.NTM.repeatSetupChoiceIdx_val (k T : ℕ) (a : Fin 2) : ↑(repeatSetupChoiceIdx k T a) = ↑a

Setup indices retain their local numeric value.

@[simp]

theorem Complexity.NTM.repeatStrideChoiceIdx_val {k : ℕ} (T : ℕ) (j : Fin k) (s : Fin (repeatAtTimeStride T)) : ↑(repeatStrideChoiceIdx T j s) = 2 + ↑j * repeatAtTimeStride T + ↑s

A stride index has the advertised row-major global position.

theorem Complexity.NTM.repeatStrideChoiceIdx_injective {k : ℕ} (T : ℕ) : Function.Injective fun (p : Fin k × Fin (repeatAtTimeStride T)) => repeatStrideChoiceIdx T p.1 p.2

Trial/offset coordinates inject into the full schedule.

theorem Complexity.NTM.repeatSetupChoiceIdx_ne_stride (k T : ℕ) (a : Fin 2) (j : Fin k) (s : Fin (repeatAtTimeStride T)) : repeatSetupChoiceIdx k T a ≠ repeatStrideChoiceIdx T j s

Setup and stride positions are disjoint.

theorem Complexity.NTM.repeatStrideChoiceIdx_sim {k : ℕ} (T : ℕ) (j : Fin k) (t : Fin T) : repeatStrideChoiceIdx T j (repeatSimulationOffset T t) = repeatChoiceIdx T j t

The generic stride embedding agrees with the machine simulation index.

theorem Complexity.NTM.repeatSimulationChoiceIdx_ne_admin {k : ℕ} (T : ℕ) (j l : Fin k) (t : Fin T) (a : Fin (T + 2)) : repeatChoiceIdx T j t ≠ repeatStrideChoiceIdx T l (repeatAdminOffset T a)

No simulation choice is an administrative choice, even across trials.

@[simp]

theorem Complexity.NTM.repeatSimulationChoices_eq_block {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) : repeatSimulationChoices choices j = (blocksEquiv k T) (repeatRandomSeed k T choices) j

A trial's simulation slice is exactly its block of the compact random seed.

@[simp]

theorem Complexity.NTM.repeatSimulationChoices_apply {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (t : Fin T) : repeatSimulationChoices choices j t = choices (repeatChoiceIdx T j t)

Pointwise form of the simulation slice.

@[simp]

theorem Complexity.NTM.repeatAdminChoices_apply {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (j : Fin k) (a : Fin (T + 2)) : repeatAdminChoices choices j a = choices (repeatStrideChoiceIdx T j (repeatAdminOffset T a))

Pointwise form of the administrative slice.

Trace prefixes at trial boundaries

def Complexity.NTM.repeatPrefixIdx (T : ℕ) {m k : ℕ} (hm : m ≤ k) : Fin (repeatAtTimeSteps m T) → Fin (repeatAtTimeSteps k T)

Include a shorter trial-boundary prefix in the full repetition schedule.

Equations

• Complexity.NTM.repeatPrefixIdx T hm i = ⟨↑i, ⋯⟩

def Complexity.NTM.repeatPrefixChoices {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (m : ℕ) (hm : m ≤ k) : Fin (repeatAtTimeSteps m T) → Bool

Restrict a full choice string to the boundary after m trials.

Equations

• Complexity.NTM.repeatPrefixChoices choices m hm i = choices (Complexity.NTM.repeatPrefixIdx T hm i)

@[simp]

theorem Complexity.NTM.repeatPrefixChoices_apply {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) (m : ℕ) (hm : m ≤ k) (i : Fin (repeatAtTimeSteps m T)) : repeatPrefixChoices choices m hm i = choices (repeatPrefixIdx T hm i)

Pointwise form of prefix restriction.

theorem Complexity.NTM.repeatPrefixChoices_self {k T : ℕ} (choices : Fin (repeatAtTimeSteps k T) → Bool) : repeatPrefixChoices choices k ⋯ = choices

Restricting at the final boundary returns the full choice string.

def Complexity.NTM.repeatBoundaryCfg {n k T : ℕ} (tm : NTM n) (x : List Bool) (choices : Fin (repeatAtTimeSteps k T) → Bool) (m : ℕ) (hm : m ≤ k) : Cfg (k * (n + 1)) (tm.RepeatQ k T)

Wrapper configuration after the exact prefix ending at trial boundary m.

Equations

• tm.repeatBoundaryCfg x choices m hm = (tm.repeatAtTime k T).trace (Complexity.NTM.repeatAtTimeSteps m T) (Complexity.NTM.repeatPrefixChoices choices m hm) ((tm.repeatAtTime k T).initCfg x)

Completed-vote and outer-boundary assertions

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

Vote vector agrees with source trials below boundary m and is false above it.

Equations

• tm.RepeatCompletedVotes x seed votes m = Complexity.NTM.RepeatVotesThrough (tm.repeatVotes x k T seed) votes m

theorem Complexity.NTM.RepeatCompletedVotes.zero {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) : tm.RepeatCompletedVotes x seed (fun (x : Fin k) => false) 0

No trials completed means every stored vote is false.

theorem Complexity.NTM.RepeatCompletedVotes.update {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (votes : Fin k → Bool) (j : Fin k) (h : tm.RepeatCompletedVotes x seed votes ↑j) : tm.RepeatCompletedVotes x seed (Function.update votes j (tm.repeatVotes x k T seed j)) (↑j + 1)

Recording trial j advances the completed-vote boundary.

theorem Complexity.NTM.RepeatCompletedVotes.eq_expected {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (votes : Fin k → Bool) (h : tm.RepeatCompletedVotes x seed votes k) : votes = tm.repeatVotes x k T seed

At the final boundary the stored vector is the complete source vote vector.

def Complexity.NTM.repeatTrialStartState {n k T : ℕ} (tm : NTM n) (j : Fin k) (votes : Fin k → Bool) : tm.RepeatQ k T

Control state at the start of trial j, including the zero-time branch.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NTM.RepeatBoundary {n k T : ℕ} (tm : NTM n) (x : List Bool) (seed : Fin (k * T) → Bool) (m : ℕ) (C : Cfg (k * (n + 1)) (tm.RepeatQ k T)) : Prop

Target assertion after m completed trials. Before the final boundary the wrapper is at the exact next-trial start with the expected vote prefix and fresh frame; at m = k it has halted with the majority verdict.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NTM.RepeatOuterClaim {n k T : ℕ} (tm : NTM n) (x : List Bool) (choices : Fin (repeatAtTimeSteps k T) → Bool) : Prop

Fully formulated outer-induction claim over every exact schedule prefix.

Equations

• tm.RepeatOuterClaim x choices = ∀ (m : ℕ) (hm : m ≤ k), tm.RepeatBoundary x (Complexity.repeatRandomSeed k T choices) m (tm.repeatBoundaryCfg x choices m hm)

theorem Complexity.NTM.RepeatOuterClaim.next {n k T : ℕ} {tm : NTM n} {x : List Bool} {choices : Fin (repeatAtTimeSteps k T) → Bool} (h : tm.RepeatOuterClaim x choices) (m : ℕ) (hm : m < k) : have j := ⟨m, hm⟩; ∃ (votes : Fin k → Bool), tm.RepeatCompletedVotes x (repeatRandomSeed k T choices) votes m ∧ (tm.repeatBoundaryCfg x choices m ⋯).state = tm.repeatTrialStartState j votes ∧ tm.repeatProjectCfg j tm.qstart (tm.repeatBoundaryCfg x choices m ⋯) = tm.initCfg x ∧ RepeatFrame x j (tm.repeatBoundaryCfg x choices m ⋯) ∧ RepeatOtherParked j (tm.repeatBoundaryCfg x choices m ⋯)

Extract the next-trial assertion from the outer claim before the last boundary.

theorem Complexity.NTM.RepeatOuterClaim.final {n k T : ℕ} {tm : NTM n} {x : List Bool} {choices : Fin (repeatAtTimeSteps k T) → Bool} (h : tm.RepeatOuterClaim x choices) : have C := tm.repeatBoundaryCfg x choices k ⋯; C.state = RepeatQ.halt ∧ C.output.head = 1 ∧ C.output.cells 1 = Γ.ofBool (majority (tm.repeatVotes x k T (repeatRandomSeed k T choices)))

Extract the final halted majority assertion from the outer claim.