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

theorem DescriptiveComplexity.ExpExpansion.exists_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} {σs : Fin n → X.pointBlock.Assignment A} (h : ∀ (i : Fin n), IsPointAssign (σs i)) : ∃ (pts : Fin n → X.Map A), stateAssign p σs = nodeState p pts ∧ σs = fun (i : Fin n) => pointAssign (pts i)

A state all of whose rounds are points carries points, and they are determined.

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'

theorem DescriptiveComplexity.ExpExpansion.nodeAt_zero_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) (pts pts' : Fin n → X.Map A) (hag : ∀ (i : Fin n), ↑i < d → pts i = pts' i) : nodeAt I hdn t 0 pts = nodeAt I hdn t 0 pts'

The first node only reads the rounds below d.

theorem DescriptiveComplexity.ExpExpansion.nodeAt_shift {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) (pts : Fin n → X.Map A) : (nodeAt I hdn t 0 fun (i : Fin n) => pts (shiftIx d n hdn i)) = nodeAt I hdn t 1 pts

Shifting the second node's rounds onto the first's reads the same node.

theorem DescriptiveComplexity.ExpExpansion.exists_pts_of_node {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) (z : I.Map (X.Map A)) (pts : Fin n → X.Map A) : ∃ (pts' : Fin n → X.Map A), (∀ (i : Fin n), ¬(d ≤ ↑i ∧ ↑i < 2 * d) → pts' i = pts i) ∧ nodeAt I hdn z.1 1 pts' = z

Every node of the graph sits in the second node's rounds of some tuple agreeing with a given one outside them.

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

theorem DescriptiveComplexity.ExpExpansion.movesFrom_startPick {T : Type} [Finite T] {d n Dm : ℕ} {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (tx : T) : movesFrom hn D hD (Ph.startPick tx) = [preEntry D hD Sub.st tx tx, { tgt := Ph.main tx, keep := keepAll n, guard := [] }]

theorem DescriptiveComplexity.ExpExpansion.movesFrom_main {T : Type} [Finite T] {d n Dm : ℕ} {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (tx : T) : movesFrom hn D hD (Ph.main tx) = preEntry D hD Sub.won tx tx :: List.flatMap (fun (ty : T) => [{ tgt := Ph.exStep tx ty, keep := keepOff n (isMid d n), guard := midRounds d n }, { tgt := Ph.allCert tx ty, keep := keepOff n (isMid d n), guard := midRounds d n }]) (finEnum T)

theorem DescriptiveComplexity.ExpExpansion.movesFrom_exStep {T : Type} [Finite T] {d n Dm : ℕ} (hdn : 2 * d ≤ n) {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (tx ty : T) : movesFrom hn D hD (Ph.exStep tx ty) = [preEntry D hD Sub.notuniv tx tx, preEntry D hD Sub.mv tx ty, { tgt := Ph.main ty, keep := keepShift d n hdn, guard := [] }]

theorem DescriptiveComplexity.ExpExpansion.movesFrom_allCert {T : Type} [Finite T] {d n Dm : ℕ} {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (tx ty : T) : movesFrom hn D hD (Ph.allCert tx ty) = preEntry D hD Sub.univ tx tx :: preEntry D hD Sub.mv tx ty :: List.map (fun (ty' : T) => { tgt := Ph.allStep tx ty', keep := keepOff n (isMid d n), guard := midRounds d n }) (finEnum T)

theorem DescriptiveComplexity.ExpExpansion.movesFrom_allStep {T : Type} [Finite T] {d n Dm : ℕ} (hdn : 2 * d ≤ n) {hn : n = 2 * d + Dm} {D : Sub → T → T → ℕ} {hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm} (tx ty : T) : movesFrom hn D hD (Ph.allStep tx ty) = [preEntry D hD Sub.notmv tx ty, { tgt := Ph.main ty, keep := keepShift d n hdn, guard := [] }]

theorem DescriptiveComplexity.ExpExpansion.moveTo_keepAll {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] {q : Ph T Dm} {pts : Fin n → X.Map A} {σs : Fin n → X.pointBlock.Assignment A} (hkeep : ∀ e ∈ keepAll n, pointAssign (pts e.1) = σs e.2) : stateAssign q σs = nodeState q pts

A move that keeps every round lands on the same points.

theorem DescriptiveComplexity.ExpExpansion.moveTo_keepShift {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (hdn : 2 * d ≤ n) {q : Ph T Dm} {pts : Fin n → X.Map A} {σs : Fin n → X.pointBlock.Assignment A} (hkeep : ∀ e ∈ keepShift d n hdn, pointAssign (pts e.1) = σs e.2) : stateAssign q σs = nodeState q fun (i : Fin n) => pts (shiftIx d n hdn i)

A shifting move carries the second node's points onto the first node's rounds.

theorem DescriptiveComplexity.ExpExpansion.moveTo_keepMid {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] {q : Ph T Dm} {pts : Fin n → X.Map A} {σs : Fin n → X.pointBlock.Assignment A} (hkeep : ∀ e ∈ keepOff n (isMid d n), pointAssign (pts e.1) = σs e.2) (hguard : ∀ i ∈ midRounds d n, IsPointAssign (σs i)) : ∃ (pts' : Fin n → X.Map A), stateAssign q σs = nodeState q pts' ∧ ∀ (i : Fin n), ¬(d ≤ ↑i ∧ ↑i < 2 * d) → pts' i = pts i

A move that guesses the second node's rounds lands on points agreeing outside them.

theorem DescriptiveComplexity.ExpExpansion.move_keepAll {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} (p : Ph T Dm) (m : MoveTo T Dm n) (hm : m ∈ movesFrom hn D hD p) (hk : m.keep = keepAll n) (hg : m.guard = []) (pts : Fin n → X.Map A) : (X.graphGame hn D hD K).Move (nodeState p pts) (nodeState m.tgt pts)

Making a move that keeps every round.

theorem DescriptiveComplexity.ExpExpansion.move_keepShift {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {d n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (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} (p : Ph T Dm) (m : MoveTo T Dm n) (hm : m ∈ movesFrom hn D hD p) (hk : m.keep = keepShift d n hdn) (hg : m.guard = []) (pts : Fin n → X.Map A) : (X.graphGame hn D hD K).Move (nodeState p pts) (nodeState m.tgt fun (i : Fin n) => pts (shiftIx d n hdn i))

Making a shifting move.

theorem DescriptiveComplexity.ExpExpansion.move_keepMid {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} (p : Ph T Dm) (m : MoveTo T Dm n) (hm : m ∈ movesFrom hn D hD p) (hk : m.keep = keepOff n (isMid d n)) (hg : m.guard = midRounds d n) (pts pts' : Fin n → X.Map A) (hag : ∀ (i : Fin n), ¬(d ≤ ↑i ∧ ↑i < 2 * d) → pts' i = pts i) : (X.graphGame hn D hD K).Move (nodeState p pts) (nodeState m.tgt pts')

Making a move that guesses the second node's rounds.

Entering a prefix decides its question

theorem DescriptiveComplexity.ExpExpansion.wins_preEntry {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)) (s : Sub) (tx ty : T) (pts : Fin n → X.Map A) : (X.graphGame hn D hD K).Wins (nodeState (preEntry D hD s tx ty).tgt pts) ↔ SubHolds I hdn s tx ty pts

Entering a prefix wins exactly when its question holds.

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.