The sentences a phased game is made of

Every game this development builds over a tag-extended block – DescriptiveComplexity.SOGameSpec.exBlock in DescriptiveComplexity.Exponential.GameSO, and the graph game that carries DescriptiveComplexity.EXPTIME to SO-GAME – says the same three things and nothing else:

• which phase a state is in, in one copy or in the second one of a move (DescriptiveComplexity.atTagF, DescriptiveComplexity.atTagTwoF);
• that the phase of the state a move enters is exactly one phase, so that a junk state – two tag bits set – is never reachable (DescriptiveComplexity.exists_tagAssign_two);
• that the listed relation variables do not change, which is how a move freezes the part of the state it must not touch (DescriptiveComplexity.varsFrozenS).

Exponential.GameSO proves these for its own block; here they are stated once for an arbitrary block and an arbitrary finite tag type, which is what the graph game needs, its states being the nodes of DescriptiveComplexity.ExpExpansion.nodeBlock – a merged tuple of rounds rather than a DescriptiveComplexity.SOBlock.cons.

The phase of a state

noncomputable def DescriptiveComplexity.atTagF (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (p : T) : ((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).Sentence

The state is a well-formed one carrying the tag p.

Equations

• DescriptiveComplexity.atTagF L C T p = C.tagGuardF T ⊓ C.tagBitF T p

noncomputable def DescriptiveComplexity.tagTwoF (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (p : T) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Sentence

The tag bit of p in the second copy of a move.

Equations

• DescriptiveComplexity.tagTwoF L C T p = FirstOrder.Language.Relations.formula (Sum.inr ⟨Sum.inl p, ⋯⟩) Fin.elim0

noncomputable def DescriptiveComplexity.atTagTwoF (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (p : T) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Sentence

The second copy of a move carries exactly the tag p: its bit is set and no other is. This is what keeps a junk state out of play.

Equations

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

Freezing part of a state

@[reducible, inline]

abbrev DescriptiveComplexity.varFstSym (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (i : C.ι) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Relations (C.arity i)

The variable i of the block, in the first copy of a move.

Equations

• DescriptiveComplexity.varFstSym L C T i = Sum.inl (Sum.inr ⟨Sum.inr i, ⋯⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.varSndSym (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (i : C.ι) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Relations (C.arity i)

The variable i of the block, in the second copy of a move.

Equations

• DescriptiveComplexity.varSndSym L C T i = Sum.inr ⟨Sum.inr i, ⋯⟩

noncomputable def DescriptiveComplexity.varAgreeS (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (i : C.ι) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Sentence

The variable i is unchanged by the move.

Equations

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

noncomputable def DescriptiveComplexity.varsFrozenS (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (vs : List C.ι) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Sentence

The listed variables are unchanged by the move.

Equations

• DescriptiveComplexity.varsFrozenS L C T vs = DescriptiveComplexity.listInf (List.map (DescriptiveComplexity.varAgreeS L C T) vs)

What they say

theorem DescriptiveComplexity.realize_atTagF {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : T) (ν : C.Assignment A) : A ⊨ atTagF L C T p ↔ p = q

theorem DescriptiveComplexity.realize_tagTwoF' {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (p : T) (σ τ : (C.withTag T).Assignment A) (x : Fin ((C.withTag T).arity (Sum.inl p)) → A) : A ⊨ tagTwoF L C T p ↔ τ (Sum.inl p) x

theorem DescriptiveComplexity.realize_tagTwoF {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : T) (σ : (C.withTag T).Assignment A) (ν : C.Assignment A) : A ⊨ tagTwoF L C T p ↔ p = q

theorem DescriptiveComplexity.realize_atTagTwoF {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : T) (σ : (C.withTag T).Assignment A) (ν : C.Assignment A) : A ⊨ atTagTwoF L C T p ↔ p = q

theorem DescriptiveComplexity.exists_tagAssign_two {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (p : T) (σ τ : (C.withTag T).Assignment A) (h : A ⊨ atTagTwoF L C T p) : τ = SOBlock.tagAssign p (SOBlock.dropTag τ)

The guarded phase of the second copy pins its shape.