The node phases play the AND/OR graph

The second correctness half: from main tx, the graph game wins exactly when the existential player wins the interpreted AND/OR graph at the node the state carries (DescriptiveComplexity.ExpExpansion.target_of_wins and DescriptiveComplexity.ExpExpansion.wins_of_winsOn). Both directions are inductions – on DescriptiveComplexity.SOGameSpec.Wins one way, on DescriptiveComplexity.WinsOn the other – and the first goes through DescriptiveComplexity.ExpExpansion.Target, which says what each of the five node phases is for.

The two places the simulation could have gone wrong, and how it does not:

• a universal node with no successor loses (WinsOn.all demands a move), so the existential player must certify a successor before the universal player chooses one – that is what allCert does, and its witness lives in the same rounds the chosen successor will;
• an illegal proposal must not count, so allStep is existential and lets the player refute AGMove instead of the move being filtered out – which no sentence over the base could do.

States whose rounds are all points

def DescriptiveComplexity.ExpExpansion.nodeState {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (p : Ph T Dm) (pts : Fin n → X.Map A) : (X.gameBlock n T Dm).Assignment A

The state at a phase whose rounds carry the given points.

Equations

• DescriptiveComplexity.ExpExpansion.nodeState p pts = DescriptiveComplexity.ExpExpansion.stateAssign p fun (i : Fin n) => DescriptiveComplexity.ExpExpansion.pointAssign (pts i)

theorem DescriptiveComplexity.ExpExpansion.pointAssign_injective {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : X.Map A) (h : pointAssign p = pointAssign q) : p = q

The nodes a state carries

theorem DescriptiveComplexity.ExpExpansion.nodeAt_congr {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d n : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (hdn : 2 * d ≤ n) (t : T) (a : Fin 2) (pts pts' : Fin n → X.Map A) (hag : ∀ (b : Fin d), pts (paramIx d n hdn a b) = pts' (paramIx d n hdn a b)) : nodeAt I hdn t a pts = nodeAt I hdn t a pts'

What each node phase is for

def DescriptiveComplexity.ExpExpansion.Target {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (hdn : 2 * d ≤ n) : Ph T Dm → (Fin n → X.Map A) → Prop

What a node phase promises. The prefix phases promise nothing: they are DescriptiveComplexity.ExpExpansion.wins_pre's business.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.ExpExpansion.Target I hdn (DescriptiveComplexity.Ph.main tx) x✝ = DescriptiveComplexity.WinsOn (I.Map (X.Map A)) (DescriptiveComplexity.ExpExpansion.nodeAt I hdn tx 0 x✝)
• DescriptiveComplexity.ExpExpansion.Target I hdn (DescriptiveComplexity.Ph.pre s tx ty j pol) x✝ = True

The moves out of the node phases

Entering a prefix decides its question

The node phases play the graph

theorem DescriptiveComplexity.ExpExpansion.target_of_wins {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (hdn : 2 * d ≤ n) {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} (hK : ∀ (s : Sub) (tx ty : T), KernelSpec I hdn (n - D s tx ty) (D s tx ty) s tx ty (K s tx ty)) (τ : (X.graphGame hn D hD K).State A) : (X.graphGame hn D hD K).Wins τ → ∀ (p : Ph T Dm) (pts : Fin n → X.Map A), τ = nodeState p pts → Target I hdn p pts

Every node phase keeps its promise.

theorem DescriptiveComplexity.ExpExpansion.wins_of_winsOn {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (I : FOInterpretation (X.E.sum FirstOrder.Language.order) FirstOrder.Language.andOrGraph T d) (hdn : 2 * d ≤ n) {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} (hK : ∀ (s : Sub) (tx ty : T), KernelSpec I hdn (n - D s tx ty) (D s tx ty) s tx ty (K s tx ty)) (x : I.Map (X.Map A)) : WinsOn (I.Map (X.Map A)) x → ∀ (tx : T) (pts : Fin n → X.Map A), x = nodeAt I hdn tx 0 pts → (X.graphGame hn D hD K).Wins (nodeState (Ph.main tx) pts)

Every win of the interpreted graph is a win of the game.