Moving whole rounds

The state of the game that carries DescriptiveComplexity.EXPTIME to SO-GAME is a tuple of rounds – DescriptiveComplexity.repMerged of the point block – carrying a phase in its tag bits. Its moves never touch one relation variable at a time: they keep a round, overwrite a round, or shift a round onto another one (the points of the node just chosen become the points the next position reads). This file states those three at the level of rounds, on top of the variable-level gadgets of DescriptiveComplexity.Exponential.GameMove.

• DescriptiveComplexity.repIx names round i's copy of a variable inside the merged block, and DescriptiveComplexity.repBlockAssign_repIx reads it back – DescriptiveComplexity.relMap_repSym stated about assignments rather than about RelMap, as DescriptiveComplexity.ExpExpansion.homAssign_roundOneIx is for a whole round.
• DescriptiveComplexity.roundsAgreeS is the move sentence “round a of the state I leave is round b of the state I enter”, one conjunct per listed pair; DescriptiveComplexity.realize_roundsAgreeS says exactly that. Freezing is the diagonal list, shifting is any other.

Nothing here mentions an expansion: a round is any block, replicated.

One round's copy of a variable

def DescriptiveComplexity.repIx (B : SOBlock) (n : ℕ) (i : Fin n) : B.ι → (repMerged B n).ι

Round i's copy of the variable x, as a relation variable of the merged block.

Equations

• DescriptiveComplexity.repIx B n i x = ↑(DescriptiveComplexity.repSym B x ⋯ n i)

theorem DescriptiveComplexity.repIx_arity (B : SOBlock) (n : ℕ) (i : Fin n) (x : B.ι) : (repMerged B n).arity (repIx B n i x) = B.arity x

theorem DescriptiveComplexity.repBlockAssign_repIx (B : SOBlock) (A : Type) (n : ℕ) (ρs : Fin n → B.Assignment A) (i : Fin n) (x : B.ι) (v : Fin (B.arity x) → A) : (repBlockAssign B A n ρs (repIx B n i x) fun (j : Fin ((repMerged B n).arity (repIx B n i x))) => v (Fin.cast ⋯ j)) ↔ ρs i x v

Reading back one variable of one round.

Whole rounds, moved

noncomputable def DescriptiveComplexity.repPairIx (B : SOBlock) (n : ℕ) (a b : Fin n) : List { p : (repMerged B n).ι × (repMerged B n).ι // (repMerged B n).arity p.2 = (repMerged B n).arity p.1 }

The variable pairs saying that round a of the first copy is round b of the second.

Equations

• DescriptiveComplexity.repPairIx B n a b = List.map (fun (x : B.ι) => ⟨(DescriptiveComplexity.repIx B n a x, DescriptiveComplexity.repIx B n b x), ⋯⟩) (DescriptiveComplexity.finEnum B.ι)

noncomputable def DescriptiveComplexity.roundPairIx (B : SOBlock) (n : ℕ) (ab : List (Fin n × Fin n)) : List { p : (repMerged B n).ι × (repMerged B n).ι // (repMerged B n).arity p.2 = (repMerged B n).arity p.1 }

The variable pairs of a list of round pairs.

Equations

• DescriptiveComplexity.roundPairIx B n ab = List.flatMap (fun (e : Fin n × Fin n) => DescriptiveComplexity.repPairIx B n e.1 e.2) ab

noncomputable def DescriptiveComplexity.roundsAgreeS (L : FirstOrder.Language) (B : SOBlock) (n : ℕ) (T : Type) [Finite T] (ab : List (Fin n × Fin n)) : (((L.sum FirstOrder.Language.order).sum ((repMerged B n).withTag T).lang).sum ((repMerged B n).withTag T).lang).Sentence

The move carries round a onto round b, for each listed pair. The diagonal list freezes the rounds it names.

Equations

• DescriptiveComplexity.roundsAgreeS L B n T ab = DescriptiveComplexity.varsPairAgreeS L (DescriptiveComplexity.repMerged B n) T (DescriptiveComplexity.roundPairIx B n ab)

theorem DescriptiveComplexity.realize_roundsAgreeS {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (p q : T) (ρs σs : Fin n → B.Assignment A) (ab : List (Fin n × Fin n)) : A ⊨ roundsAgreeS L B n T ab ↔ ∀ e ∈ ab, ρs e.1 = σs e.2

What moving rounds says: the listed rounds of the state the move leaves are the corresponding rounds of the state it enters.