The atoms of the translation

An atom of a sentence over an expansion says one of three things about the points its variables hold: that a relation of the expanded vocabulary holds of them, that two of them are equal, or that one is below another. This file writes each of those as a sentence of the quantifier prefix, and proves it right.

All three follow one pattern. The corresponding sentence of the expansion – DescriptiveComplexity.ExpExpansion.relSentence, DescriptiveComplexity.SOBlock.eqAssignF, DescriptiveComplexity.ExpExpansion.ordSentence – is indexed by a static tuple of tags, because everywhere else in this development a tag is chosen at formula-construction time. Here the tags are guessed, so the sentence appears once per tuple of tags, guarded by the tag bits of the rounds involved (DescriptiveComplexity.ExpExpansion.roundTagBitF). Finitely many tuples, so the disjunction is a DescriptiveComplexity.listSup; exactly one bit per round is set, so exactly one disjunct can fire.

Equality is the exception and is cheaper: rather than a disjunction over tag pairs it compares the tag bits round by round, which says the tags agree without naming them.

def DescriptiveComplexity.ExpExpansion.roundAssign {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (pts : Fin m → X.Map A) : Fin m → X.pointBlock.Assignment A

The rounds of the prefix that hold a given tuple of points.

Equations

• DescriptiveComplexity.ExpExpansion.roundAssign pts i = DescriptiveComplexity.SOBlock.tagAssign (↑(pts i)).1 (↑(pts i)).2

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.prefixStructure {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (pts : Fin m → X.Map A) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Structure A

The structure the kernel of the translation is realized against.

Equations

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

The tag bits of a round

noncomputable def DescriptiveComplexity.ExpExpansion.roundTagBitF {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) (i : Fin m) (t : X.Tag) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

The atom “round i carries the tag t”: the tag bit of the guessed point, read at that round.

Equations

• X.roundTagBitF m i t = (DescriptiveComplexity.ExpExpansion.roundOneLHom i X).onSentence (X.B.tagBitF X.Tag t)

theorem DescriptiveComplexity.ExpExpansion.realize_roundTagBitF {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (pts : Fin m → X.Map A) (i : Fin m) (t : X.Tag) : A ⊨ X.roundTagBitF m i t ↔ t = (↑(pts i)).1

noncomputable def DescriptiveComplexity.ExpExpansion.roundPointGuardF {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) (i : Fin m) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

The guard “round i holds a point of the expanded universe”, read at that round: what a peeled quantifier carries.

Equations

• X.roundPointGuardF m i = (DescriptiveComplexity.ExpExpansion.roundOneLHom i X).onSentence X.pointGuardF

theorem DescriptiveComplexity.ExpExpansion.realize_roundPointGuardF {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin m → X.pointBlock.Assignment A) (i : Fin m) : A ⊨ X.roundPointGuardF m i ↔ ∃ (t : X.Tag) (ρ : X.B.Assignment A), ρs i = SOBlock.tagAssign t ρ ∧ DomHolds (t, ρ)

Equality of two points

noncomputable def DescriptiveComplexity.ExpExpansion.pointEqF {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) (i₀ i₁ : Fin m) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

The atom “the points of rounds i₀ and i₁ are equal”: their tag bits agree round by round, and their assignments hold of the same atoms.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_pointEqF {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (pts : Fin m → X.Map A) (i₀ i₁ : Fin m) : A ⊨ X.pointEqF m i₀ i₁ ↔ pts i₀ = pts i₁

A relation of the expanded vocabulary

noncomputable def DescriptiveComplexity.ExpExpansion.pointRelF {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) {k : ℕ} (r : X.E.Relations k) (idx : Fin k → Fin m) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

The atom “the relation r holds of the points of the rounds idx”: one disjunct per tuple of tags, guarded by the tag bits of those rounds.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_pointRelF {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (pts : Fin m → X.Map A) {k : ℕ} (r : X.E.Relations k) (idx : Fin k → Fin m) : A ⊨ X.pointRelF m r idx ↔ FirstOrder.Language.Structure.RelMap r fun (j : Fin k) => pts (idx j)

The order on two points

noncomputable def DescriptiveComplexity.ExpExpansion.pointLeF {L : FirstOrder.Language} (X : ExpExpansion L) (m : ℕ) (i₀ i₁ : Fin m) : ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock m).lang).Sentence

The atom “the point of round i₀ is below that of round i₁”: one disjunct per pair of tags, guarded by the two tag bits.

Equations

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

theorem DescriptiveComplexity.ExpExpansion.realize_pointLeF {L : FirstOrder.Language} {X : ExpExpansion L} {m : ℕ} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (pts : Fin m → X.Map A) (i₀ i₁ : Fin m) : A ⊨ X.pointLeF m i₀ i₁ ↔ pts i₀ ≤ pts i₁