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.moveFstLHom_isExpansionOn {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (σ τ : (C.withTag T).Assignment A) : (moveFstLHom L C T).IsExpansionOn A

theorem DescriptiveComplexity.moveSndLHom_isExpansionOn {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (σ τ : (C.withTag T).Assignment A) : (moveSndLHom L C T).IsExpansionOn A

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.

theorem DescriptiveComplexity.realize_tagFst {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.withTag T).lang).Sentence) : A ⊨ FirstOrder.Language.LHom.sumInl.onSentence ψ ↔ A ⊨ ψ

A sentence about the state a move leaves, tag bits included. Unlike DescriptiveComplexity.realize_moveFstLHom this reads a sentence over the tagged block, which is what a move's guard on its own phase (DescriptiveComplexity.atTagF) is.

theorem DescriptiveComplexity.eq_tagAssign_of_atTagF {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 ⊨ atTagF L C T p) : σ = SOBlock.tagAssign p (SOBlock.dropTag σ)

A state at a phase is a tagged one. DescriptiveComplexity.atTagF is the one-copy counterpart of DescriptiveComplexity.exists_tagAssign_two: a start sentence that asserts it admits no junk assignment.

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.

theorem DescriptiveComplexity.realize_varPairAgreeS {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (σ τ : (C.withTag T).Assignment A) (i j : C.ι) (h : C.arity j = C.arity i) : A ⊨ varPairAgreeS L C T i j h ↔ ∀ (x : Fin (C.arity i) → A), σ (Sum.inr i) x ↔ τ (Sum.inr j) fun (k : Fin ((C.withTag T).arity (Sum.inr j))) => x (Fin.cast h k)

theorem DescriptiveComplexity.realize_varsPairAgreeS {L : FirstOrder.Language} {C : SOBlock} {T : Type} [Finite T] {A : Type} [instL : L.Structure A] [LinearOrder A] (σ τ : (C.withTag T).Assignment A) (ps : List { p : C.ι × C.ι // C.arity p.2 = C.arity p.1 }) : A ⊨ varsPairAgreeS L C T ps ↔ ∀ p ∈ ps, ∀ (x : Fin (C.arity (↑p).1) → A), σ (Sum.inr (↑p).1) x ↔ τ (Sum.inr (↑p).2) fun (k : Fin ((C.withTag T).arity (Sum.inr (↑p).2))) => x (Fin.cast ⋯ k)