Reading a block sentence in a copy, and moving one variable onto another

Two gadgets every phased game needs beyond DescriptiveComplexity.Exponential.GamePhase, both stated for an arbitrary block C and finite tag type T.

• A one-copy sentence, read in a copy of a move. The four sentences of a DescriptiveComplexity.SOGameSpec live at three different vocabularies, and everything a move says about one of its two states is a sentence over (L + ≤) + C.lang – the leaf kernel of a quantifier prefix, a guard, the order. DescriptiveComplexity.moveFstLHom and DescriptiveComplexity.moveSndLHom read such a sentence in the first and in the second copy, dropping the tag bits, and DescriptiveComplexity.realize_moveFstLHom / DescriptiveComplexity.realize_moveSndLHom say so.

• One variable moved onto another. DescriptiveComplexity.varsFrozenS freezes a variable in place, which is what a move that must not disturb the state says. DescriptiveComplexity.varPairAgreeS is the same statement between two different variables of equal arity – the first copy's i and the second copy's j – which is what a move that shifts part of the state says: copying the points of the node just chosen onto the slots the next position reads them from. Freezing is the diagonal case j = i.

A one-copy sentence, read in a copy

def DescriptiveComplexity.moveFstLHom (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] : (L.sum FirstOrder.Language.order).sum C.lang →ᴸ ((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang

A sentence about one assignment of C, read in the first copy of a move: the tag bits are invisible to it.

Equations

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

def DescriptiveComplexity.moveSndLHom (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] : (L.sum FirstOrder.Language.order).sum C.lang →ᴸ ((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang

A sentence about one assignment of C, read in the second copy of a move – the state the move enters.

Equations

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

theorem DescriptiveComplexity.realize_moveFstLHom {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (σ τ : (C.withTag T).Assignment A) (ψ : ((L.sum FirstOrder.Language.order).sum C.lang).Sentence) : A ⊨ (moveFstLHom L C T).onSentence ψ ↔ A ⊨ ψ

The first copy of a move is the state it leaves.

theorem DescriptiveComplexity.realize_moveSndLHom {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (σ τ : (C.withTag T).Assignment A) (ψ : ((L.sum FirstOrder.Language.order).sum C.lang).Sentence) : A ⊨ (moveSndLHom L C T).onSentence ψ ↔ A ⊨ ψ

The second copy of a move is the state it enters.

One variable moved onto another

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

The move copies the variable i of the state it leaves onto the variable j of the state it enters. With j = i this is DescriptiveComplexity.varAgreeS, i.e., freezing.

Equations

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

noncomputable def DescriptiveComplexity.varsPairAgreeS (L : FirstOrder.Language) (C : SOBlock) (T : Type) [Finite T] (ps : List { p : C.ι × C.ι // C.arity p.2 = C.arity p.1 }) : (((L.sum FirstOrder.Language.order).sum (C.withTag T).lang).sum (C.withTag T).lang).Sentence

The listed variables are moved into place by the move.

Equations

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