A guessed block that is a point of the expanded universe

DescriptiveComplexity.SOBlock.tagGuardF says a guessed assignment names a tag. A quantifier of the translation lemma ranges over the points of X.Map A, which is less: a point must also satisfy its tag's domain sentence. This file conjoins the two into DescriptiveComplexity.ExpExpansion.pointGuardF, the guard every peeled quantifier carries – existentially as a conjunct, universally as a hypothesis.

The only new bookkeeping is reading X.dom t, a sentence over the block X.B, inside the tag-extended block X.B.withTag X.Tag. That is DescriptiveComplexity.SOBlock.homLHom at the inclusion Sum.inr, whose arity condition is rfl and whose transported assignment is DescriptiveComplexity.SOBlock.dropTag exactly – so the transport lemma is DescriptiveComplexity.SOBlock.realize_homSentence with nothing to prove.

The domain sentence is selected by the tag bits rather than statically, so it appears once per tag, guarded by that tag's bit. Exactly one bit is set, so exactly one of those implications has a true hypothesis.

Reading a block sentence inside the tag-extended block

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

The inclusion of a block into its tag extension, as a vocabulary map: the tag variables are simply not mentioned.

Equations

• DescriptiveComplexity.ExpExpansion.withTagLHom L B T = (FirstOrder.Language.LHom.id (L.sum FirstOrder.Language.order)).sumMap (DescriptiveComplexity.SOBlock.homLHom Sum.inr ⋯)

theorem DescriptiveComplexity.ExpExpansion.realize_withTagLHom {L : FirstOrder.Language} {B : SOBlock} {T : Type} [Finite T] {A : Type} [L.Structure A] [LinearOrder A] (σ : (B.withTag T).Assignment A) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : A ⊨ (withTagLHom L B T).onSentence φ ↔ A ⊨ φ

Reading a block sentence in the extension is reading it at the dropped assignment: the tag bits are invisible to it.

The point guard

noncomputable def DescriptiveComplexity.ExpExpansion.pointGuardF {L : FirstOrder.Language} (X : ExpExpansion L) : ((L.sum FirstOrder.Language.order).sum (X.B.withTag X.Tag).lang).Sentence

The guard saying a guessed block is a point of the expanded universe: its tag bits name a tag, and its assignment satisfies that tag's domain sentence.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_pointGuardF {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (σ : (X.B.withTag X.Tag).Assignment A) : A ⊨ X.pointGuardF ↔ ∃ (t : X.Tag) (ρ : X.B.Assignment A), σ = SOBlock.tagAssign t ρ ∧ DomHolds (t, ρ)

The guard is exactly “this is a point”.