The graph game, as a second-order alternating game

The four sentences of DescriptiveComplexity.ExpExpansion.graphGame, and what each of them says. Every one is a static disjunction over the phase type, which is finite: the phases carry the tags of the two nodes a state holds, so naming a tag costs a disjunct rather than a quantifier.

• univ – the phases DescriptiveComplexity.Ph.IsUniv selects, and nothing else;
• won – a leaf pre s tx ty 0 pol, conjoined with that question's kernel. The leaf is existential and has no move, so a false kernel loses: a player who asked for a proof he cannot give is stuck there;
• start – a startPick phase whose rounds all hold points (DescriptiveComplexity.ExpExpansion.allRoundsPointF), which is the invariant every node move preserves and every prefix consumes;
• move – one disjunct per pair of a phase and one of the moves DescriptiveComplexity.ExpExpansion.movesFrom allows out of it. A move names its target phase exactly (DescriptiveComplexity.atTagTwoF, so no junk state is reachable), lists the rounds it carries over – kept, shifted, or neither – and lists the rounds of the state it enters that it guards to be points.

The one asymmetry worth naming: the move that fills a play round guards nothing. DescriptiveComplexity.altBlockQuant ranges over all assignments and the point guards of a prefix live inside its kernel (DescriptiveComplexity.ExpExpansion.stepF), so guarding there would count them twice and break the correspondence with DescriptiveComplexity.ExpExpansion.exists_paramKernel.

The rounds a move carries over

def DescriptiveComplexity.keepAll (n : ℕ) : List (Fin n × Fin n)

Carry over every round: the move freezes the state.

Equations

• DescriptiveComplexity.keepAll n = List.map (fun (i : Fin n) => (i, i)) (List.finRange n)

def DescriptiveComplexity.keepOff (n : ℕ) (S : Fin n → Bool) : List (Fin n × Fin n)

Carry over every round outside S, in place.

Equations

• DescriptiveComplexity.keepOff n S = List.map (fun (i : Fin n) => (i, i)) (List.filter (fun (i : Fin n) => !S i) (List.finRange n))

def DescriptiveComplexity.isMid (d n : ℕ) : Fin n → Bool

The rounds holding the second node's points.

Equations

• DescriptiveComplexity.isMid d n i = decide (d ≤ ↑i ∧ ↑i < 2 * d)

def DescriptiveComplexity.midRounds (d n : ℕ) : List (Fin n)

The rounds holding the second node's points, as a list.

Equations

• DescriptiveComplexity.midRounds d n = List.filter (DescriptiveComplexity.isMid d n) (List.finRange n)

def DescriptiveComplexity.shiftIx (d n : ℕ) (h : 2 * d ≤ n) (i : Fin n) : Fin n

Where round i of the state a shifting move enters reads from: the second node's points become the first node's.

Equations

• DescriptiveComplexity.shiftIx d n h i = if hi : ↑i < d then ⟨↑i + d, ⋯⟩ else i

def DescriptiveComplexity.keepShift (d n : ℕ) (h : 2 * d ≤ n) : List (Fin n × Fin n)

Carry the second node's points onto the first node's slots.

Equations

• DescriptiveComplexity.keepShift d n h = List.map (fun (i : Fin n) => (DescriptiveComplexity.shiftIx d n h i, i)) (List.finRange n)

theorem DescriptiveComplexity.forall_keepAll {n : ℕ} {α : Type} (ρs σs : Fin n → α) : (∀ e ∈ keepAll n, ρs e.1 = σs e.2) ↔ ρs = σs

theorem DescriptiveComplexity.forall_keepOff {n : ℕ} {α : Type} (S : Fin n → Bool) (ρs σs : Fin n → α) : (∀ e ∈ keepOff n S, ρs e.1 = σs e.2) ↔ ∀ (i : Fin n), S i = false → ρs i = σs i

theorem DescriptiveComplexity.forall_keepShift {d n : ℕ} {α : Type} (h : 2 * d ≤ n) (ρs σs : Fin n → α) : (∀ e ∈ keepShift d n h, ρs e.1 = σs e.2) ↔ ∀ (i : Fin n), ρs (shiftIx d n h i) = σs i

theorem DescriptiveComplexity.mem_midRounds {d n : ℕ} (i : Fin n) : i ∈ midRounds d n ↔ d ≤ ↑i ∧ ↑i < 2 * d

theorem DescriptiveComplexity.isMid_eq_false {d n : ℕ} (i : Fin n) : isMid d n i = false ↔ ¬(d ≤ ↑i ∧ ↑i < 2 * d)

The moves out of a phase

structure DescriptiveComplexity.MoveTo (T : Type) (Dm n : ℕ) : Type

A move of the graph game, seen from the phase it leaves: where it goes, which rounds it carries over – as pairs (round of the state left, round of the state entered) – and which rounds of the state entered it guards to hold a point.

• tgt : Ph T Dm

  The phase the move enters.

• keep : List (Fin n × Fin n)

  The rounds it carries over.

• guard : List (Fin n)

  The rounds of the state it enters that it guards to hold a point.

def DescriptiveComplexity.ExpExpansion.preEntry {T : Type} {n Dm : ℕ} (D : Sub → T → T → ℕ) (hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm) (s : Sub) (tx ty : T) : MoveTo T Dm n

Entering the prefix that decides the question s about the nodes tagged tx, ty: nothing moves, and all D s tx ty play rounds are still to fill.

Equations

• DescriptiveComplexity.ExpExpansion.preEntry D hD s tx ty = { tgt := DescriptiveComplexity.Ph.pre s tx ty ⟨D s tx ty, ⋯⟩ true, keep := DescriptiveComplexity.keepAll n, guard := [] }

noncomputable def DescriptiveComplexity.ExpExpansion.movesFrom {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) : Ph T Dm → List (MoveTo T Dm n)

The moves out of each phase. This is the game.

Equations

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

The four sentences

noncomputable def DescriptiveComplexity.ExpExpansion.moveOf {L : FirstOrder.Language} (X : ExpExpansion L) {T : Type} [Finite T] {n Dm : ℕ} (p : Ph T Dm) (m : MoveTo T Dm n) : (((L.sum FirstOrder.Language.order).sum (X.gameBlock n T Dm).lang).sum (X.gameBlock n T Dm).lang).Sentence

The sentence of one move: it names the phase it leaves and the phase it enters, carries its rounds over, and guards the rounds it says are points.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.graphGame {L : FirstOrder.Language} (X : ExpExpansion L) {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) (K : Sub → T → T → ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence) : SOGameSpec L

The graph game: the game whose positions are the nodes of the AND/OR graph an interpretation draws on the expanded universe, together with the prefix positions that decide the six questions about them.

Equations

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

What the four sentences say

theorem DescriptiveComplexity.ExpExpansion.realize_moveOf {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (p' p q : Ph T Dm) (m : MoveTo T Dm n) (ρs σs : Fin n → X.pointBlock.Assignment A) : A ⊨ X.moveOf p' m ↔ p' = p ∧ m.tgt = q ∧ (∀ e ∈ m.keep, ρs e.1 = σs e.2) ∧ ∀ i ∈ m.guard, IsPointAssign (σs i)

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.stateStructure {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (σ : (X.gameBlock n T Dm).Assignment A) : ((L.sum FirstOrder.Language.order).sum (X.gameBlock n T Dm).lang).Structure A

The one-copy structure a state of the graph game is read against.

Equations

• DescriptiveComplexity.ExpExpansion.stateStructure σ = (X.gameBlock n T Dm).structure₁ σ

theorem DescriptiveComplexity.ExpExpansion.graphGame_isUniv {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) (ρs : Fin n → X.pointBlock.Assignment A) : (X.graphGame hn D hD K).IsUniv (stateAssign p ρs) ↔ p.IsUniv

The universal positions are the phases Ph.IsUniv names.

theorem DescriptiveComplexity.ExpExpansion.graphGame_isWon {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) (ρs : Fin n → X.pointBlock.Assignment A) : (X.graphGame hn D hD K).IsWon (stateAssign p ρs) ↔ ∃ (s : Sub) (tx : T) (ty : T) (pol : Bool), p = Ph.pre s tx ty ⟨0, ⋯⟩ pol ∧ A ⊨ K s tx ty

The positions that win outright are the leaves whose kernel holds.

theorem DescriptiveComplexity.ExpExpansion.graphGame_isStart {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} (τ : (X.gameBlock n T Dm).Assignment A) : (X.graphGame hn D hD K).IsStart τ ↔ ∃ (tx : T) (pts : Fin n → X.Map A), τ = stateAssign (Ph.startPick tx) fun (i : Fin n) => pointAssign (pts i)

The starting positions are the startPick states whose rounds are all points.

theorem DescriptiveComplexity.ExpExpansion.graphGame_move {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 q : Ph T Dm) (ρs σs : Fin n → X.pointBlock.Assignment A) : (X.graphGame hn D hD K).Move (stateAssign p ρs) (stateAssign q σs) ↔ ∃ m ∈ movesFrom hn D hD p, m.tgt = q ∧ (∀ e ∈ m.keep, ρs e.1 = σs e.2) ∧ ∀ i ∈ m.guard, IsPointAssign (σs i)

The moves are the listed ones.

theorem DescriptiveComplexity.ExpExpansion.graphGame_move_shape {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} {ρs : Fin n → X.pointBlock.Assignment A} {τ : (X.gameBlock n T Dm).Assignment A} (h : (X.graphGame hn D hD K).Move (stateAssign p ρs) τ) : ∃ (q : Ph T Dm) (σs : Fin n → X.pointBlock.Assignment A), τ = stateAssign q σs

Every move lands on a state: each disjunct pins the tag bits of the state it enters, so a junk assignment is never reachable.