The prefix phases play the alternating prefix

The first of the two correctness halves of the graph game: from a phase pre s tx ty j pol, the game plays exactly j more rounds, alternating from pol, and is then decided by the kernel of the question s (DescriptiveComplexity.ExpExpansion.wins_pre). The proof is a plain induction on j against DescriptiveComplexity.altBlockQuant's own recursion – which is what carrying the polarity in the phase buys.

Two things make the base and the step line up.

• A leaf is existential and moveless. movesFrom returns [] at j = 0 and Ph.IsUniv is false there, so the position wins exactly when it wins outright, i.e., exactly when the kernel holds. A question the player cannot prove therefore loses, which is the whole point of asking it as a move.
• Filling a round is changing one round. The move out of pre … (j+1) … freezes every round but n - (j + 1), and DescriptiveComplexity.ExpExpansion.fillRounds_succ is the identity between filling j + 1 rounds of the state left and filling j rounds of the state entered.

Fin.cons at an index known by its value

Filling the last rounds

noncomputable def DescriptiveComplexity.ExpExpansion.fillRounds {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} {k : ℕ} (hk : k ≤ n) (ρs : Fin n → X.pointBlock.Assignment A) (τs : Fin k → X.pointBlock.Assignment A) : Fin n → X.pointBlock.Assignment A

The rounds ρs with the last k overwritten by τs, in order.

Equations

• DescriptiveComplexity.ExpExpansion.fillRounds hk ρs τs i = if x : n - k ≤ ↑i then τs ⟨↑i - (n - k), ⋯⟩ else ρs i

theorem DescriptiveComplexity.ExpExpansion.fillRounds_zero {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} (hk : 0 ≤ n) (ρs : Fin n → X.pointBlock.Assignment A) (τs : Fin 0 → X.pointBlock.Assignment A) : fillRounds hk ρs τs = ρs

theorem DescriptiveComplexity.ExpExpansion.fillRounds_succ {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} (k : ℕ) (hk : k + 1 ≤ n) (ρs σs : Fin n → X.pointBlock.Assignment A) (τs : Fin k → X.pointBlock.Assignment A) (r : Fin n) (hr : ↑r = n - (k + 1)) (hag : ∀ (i : Fin n), i ≠ r → ρs i = σs i) : fillRounds hk ρs (Fin.cons (σs r) τs) = fillRounds ⋯ σs τs

Filling one more round is filling one fewer round of the state the move enters, provided that state differs from the one it leaves only at the round being filled.

The moves out of a prefix phase

The prefix phases

theorem DescriptiveComplexity.ExpExpansion.wins_pre {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} {K : Sub → T → T → ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence} (k : ℕ) (hk : k < Dm + 1) (pol : Bool) (s : Sub) (tx ty : T) (ρs : Fin n → X.pointBlock.Assignment A) : (X.graphGame hn D hD K).Wins (stateAssign (Ph.pre s tx ty ⟨k, hk⟩ pol) ρs) ↔ altBlockQuant A X.pointBlock k (fun (τs : Fin k → X.pointBlock.Assignment A) => A ⊨ K s tx ty) pol

A prefix phase plays the prefix. From pre s tx ty j pol the game fills the last j rounds, alternating from pol, and the kernel of s decides the leaf.