Placing an expansion's sentences into a quantifier prefix #

The translation lemma quantifies m points of the expanded universe, one per quantifier of the sentence being translated. Its kernel then has to talk about those points – and everything it can say about them is already written, in DescriptiveComplexity.ExpExpansion.relSentence, DescriptiveComplexity.ExpExpansion.ordSentence and DescriptiveComplexity.SOBlock.eqAssignF. All three are sentences over the ordered base expanded by DescriptiveComplexity.SOBlock.replicate n – n copies of the expansion's block, one per argument.

What this file supplies is the renaming that reads such a sentence inside the quantifier prefix: copy j of X.B is to be read as the X.B-part of round sel j.

The prefix itself is not built here and needs nothing new. DescriptiveComplexity.SecondOrderReplicate already collapses m copies of one block into a single merged block (DescriptiveComplexity.repMerged), names each round's variables (DescriptiveComplexity.repSym) and identifies the alternating quantification over the merged assignment with one assignment per round (DescriptiveComplexity.sorealize_repBlocks). So the kernel is a sentence over one merged block, and the renaming below is a DescriptiveComplexity.SOBlock.homLHom between two blocks – no bespoke m-block expansion is needed anywhere.

The one fact with content is DescriptiveComplexity.ExpExpansion.homAssign_roundIx: transporting a merged assignment back along the renaming gives the replicated assignment of the selected rounds, with their tag bits dropped. It is relMap_repSym read as a statement about assignments rather than about RelMap.

source

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.pointBlock {L : FirstOrder.Language} (X : ExpExpansion L) :

SOBlock

The block one quantified point of the expanded universe is guessed in: the expansion's block, extended by its tag bits.

Equations

X.pointBlock = X.B.withTag X.Tag

Instances For

Dependency graph

The renaming #

source

def DescriptiveComplexity.ExpExpansion.roundIx {L : FirstOrder.Language} {m n : ℕ} (sel : Fin n → Fin m) (X : ExpExpansion L) :

(X.B.replicate n).ι → (repMerged X.pointBlock m).ι

Copy j of the expansion's block, read as the X.B-part of round sel j.

Equations

DescriptiveComplexity.ExpExpansion.roundIx sel X p = ↑(DescriptiveComplexity.repSym X.pointBlock (Sum.inr p.2) ⋯ m (sel p.1))

Instances For

Dependency graph

source

theorem DescriptiveComplexity.ExpExpansion.roundIx_arity {L : FirstOrder.Language} {m n : ℕ} (sel : Fin n → Fin m) (X : ExpExpansion L) (p : (X.B.replicate n).ι) :

(repMerged X.pointBlock m).arity (roundIx sel X p) = (X.B.replicate n).arity p

Dependency graph

source

def DescriptiveComplexity.ExpExpansion.roundLHom {L : FirstOrder.Language} {m n : ℕ} (sel : Fin n → Fin m) (X : ExpExpansion L) :

(L.sum FirstOrder.Language.order).sum (X.B.replicate n).lang →ᴸ (L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang

The vocabulary map reading a sentence over n copies of the expansion's block inside the quantifier prefix, copy j at round sel j.

Equations

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

Instances For

Dependency graph

Correctness #

source

theorem DescriptiveComplexity.ExpExpansion.homAssign_roundIx {L : FirstOrder.Language} {m n : ℕ} (sel : Fin n → Fin m) {A : Type} (X : ExpExpansion L) (ρs : Fin m → X.pointBlock.Assignment A) :

SOBlock.homAssign (roundIx sel X) ⋯ (repBlockAssign X.pointBlock A m ρs) = X.B.replicateAssign fun (j : Fin n) => SOBlock.dropTag (ρs (sel j))

Transporting the prefix's assignment back along the renaming gives the n selected rounds, with their tag bits dropped. This is DescriptiveComplexity.relMap_repSym read as a statement about assignments.

Dependency graph

source

theorem DescriptiveComplexity.ExpExpansion.realize_roundLHom {L : FirstOrder.Language} {m n : ℕ} (sel : Fin n → Fin m) {A : Type} [L.Structure A] [LinearOrder A] (X : ExpExpansion L) (ρs : Fin m → X.pointBlock.Assignment A) (φ : ((L.sum FirstOrder.Language.order).sum (X.B.replicate n).lang).Sentence) :

A ⊨ (roundLHom sel X).onSentence φ ↔ A ⊨ φ

The renaming is correct: a sentence over n copies of the expansion's block, read inside the prefix, says of the selected rounds what it said of the copies.

Dependency graph

Reading one whole round #

The selection above places a sentence about n arguments of the expansion's block. A sentence about a whole guessed point – its tag bits included, so DescriptiveComplexity.SOBlock.tagBitF and DescriptiveComplexity.ExpExpansion.pointGuardF – needs the same renaming at X.pointBlock rather than at X.B. It is the same construction with sel replaced by a single round.

source