Reading an expansion's defining sentences through the meanings

A defining sentence of an exponential expansion – the sentence that says whether a relation of the expanded vocabulary holds of k points – is written over the ordered base vocabulary expanded by k copies of the expansion's block (DescriptiveComplexity.ExpExpansion.relSentence). Value invention holds those k points as k invented values of one extended universe, each standing for an assignment of the block through a guessed meaning relation. So the sentence has to be read with:

• its base symbols passing through untouched, but among the original elements only;
• its order symbol at a guessed linear order, the extended universe having none of its own;
• the block symbol of copy i and variable j read as Mⱼ vᵢ ·, the meaning relation of j at the value the copy holds.

That is a DescriptiveComplexity.ParamHom – the third item changes a symbol's arity and puts a free variable in front of its arguments – followed by relativization to the original elements, which DescriptiveComplexity.ParamHom.relOnSentenceF performs in one step.

What this file adds is the map itself (DescriptiveComplexity.readHom) and what it is worth (DescriptiveComplexity.realize_readHom): the structure the map induces on the original elements is the base structure expanded by the k copies of the block, interpreted by the assignments the values mean. The three hypotheses that buy it name the three items above, each as a plain statement about the target structure rather than about a formula.

The target vocabulary is left abstract, a DescriptiveComplexity.ReadSyms naming only the symbols the translation uses: the assembly that puts the order, the meanings, the tag bits and a guessed certificate into one block chooses where each of them sits, and nothing here needs to know.

The symbols the translation uses

structure DescriptiveComplexity.ReadSyms (L : FirstOrder.Language) (B : SOBlock) (Lt : FirstOrder.Language) : Type

The symbols a translation through the meanings needs in the target vocabulary: the base vocabulary's own, a binary symbol for the guessed order, and one meaning symbol per variable of the block, of that variable's arity plus one.

• base {n : ℕ} : L.Relations n → Lt.Relations n

  The image of a base symbol.

• ord : Lt.Relations 2

  The symbol the guessed order is read at.

• mean (i : B.ι) : Lt.Relations (B.arity i + 1)

  The meaning relation of a variable: its arity, plus the value it belongs to.

The map

def DescriptiveComplexity.readHom {L Lt : FirstOrder.Language} {B : SOBlock} (S : ReadSyms L B Lt) (k : ℕ) [L.IsRelational] : ParamHom ((L.sum FirstOrder.Language.order).sum (B.replicate k).lang) Lt (Fin k)

The translation: base symbols through, the order symbol at the guessed order, and the block symbol of copy i at the meaning relation of its variable, with the value of copy i as first argument.

Equations

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

def DescriptiveComplexity.readHom₁ {L Lt : FirstOrder.Language} {B : SOBlock} (S : ReadSyms L B Lt) [L.IsRelational] : ParamHom ((L.sum FirstOrder.Language.order).sum B.lang) Lt Unit

The same at a single copy, which is the shape a domain sentence has: DescriptiveComplexity.ExpExpansion.dom speaks of one assignment, so its block symbols are the block's own and there is one value to read them at.

Equations

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

What it is worth

structure DescriptiveComplexity.ReadOn {L Lt : FirstOrder.Language} {B : SOBlock} {M A : Type} [Lt.Structure M] [L.Structure A] [LinearOrder A] (S : ReadSyms L B Lt) (e : A → M) (means : M → B.Assignment A) : Prop

The three readings the translation promises, as statements about the target structure: base symbols hold of original elements as they do in the instance, the order symbol is the instance's order, and the meaning symbol of a variable, at a value, is the assignment that value means.

• base {n : ℕ} (r : L.Relations n) (ts : Fin n → A) : (FirstOrder.Language.Structure.RelMap (S.base r) fun (i : Fin n) => e (ts i)) ↔ FirstOrder.Language.Structure.RelMap r ts

  A base symbol holds of original elements exactly as it does in the instance.

• ord (ts : Fin 2 → A) : (FirstOrder.Language.Structure.RelMap S.ord fun (i : Fin 2) => e (ts i)) ↔ ts 0 ≤ ts 1

  The order symbol is the instance's order.

• mean (v : M) (i : B.ι) (ts : Fin (B.arity i) → A) : (FirstOrder.Language.Structure.RelMap (S.mean i) fun (i_1 : Fin (B.arity i + 1)) => Fin.cases v (fun (j : Fin (B.arity i)) => e (ts j)) i_1) ↔ means v i ts

  The meaning symbol of a variable, at a value, is the assignment that value means.

theorem DescriptiveComplexity.readEquiv_rel {L Lt : FirstOrder.Language} {B : SOBlock} {S : ReadSyms L B Lt} {k : ℕ} {M A : Type} [Lt.Structure M] [L.IsRelational] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → B.Assignment A} (h : ReadOn S e means) (vs : Fin k → M) {n : ℕ} (r : ((L.sum FirstOrder.Language.order).sum (B.replicate k).lang).Relations n) (x : Fin n → A) : FirstOrder.Language.Structure.RelMap r x ↔ FirstOrder.Language.Structure.RelMap r x

The structure the translation induces on the original elements agrees, symbol by symbol, with the base structure expanded by the k copies of the block interpreted by the assignments the values mean.

def DescriptiveComplexity.readEquiv {L Lt : FirstOrder.Language} {B : SOBlock} {S : ReadSyms L B Lt} {k : ℕ} {M A : Type} [Lt.Structure M] [L.IsRelational] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → B.Assignment A} (h : ReadOn S e means) (vs : Fin k → M) : ((L.sum FirstOrder.Language.order).sum (B.replicate k).lang).Equiv A A

The structure the translation induces on the original elements is the one the defining sentence is meant to be read in: the base structure, its order, and one copy of the block per value, interpreted by the assignment that value means.

Equations

• DescriptiveComplexity.readEquiv h vs = { toEquiv := Equiv.refl A, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.realize_readHom {L Lt : FirstOrder.Language} {B : SOBlock} {S : ReadSyms L B Lt} {k : ℕ} {M A : Type} [Lt.Structure M] [L.IsRelational] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → B.Assignment A} (h : ReadOn S e means) {R : Lt.Relations 1} (hinj : Function.Injective e) (hR : ∀ (x : M), FirstOrder.Language.Structure.RelMap R ![x] ↔ ∃ (a : A), e a = x) (vs : Fin k → M) (φ : ((L.sum FirstOrder.Language.order).sum (B.replicate k).lang).Sentence) : ((readHom S k).relOnSentenceF R φ).Realize vs ↔ A ⊨ φ

The translation, read among the original elements, says what the defining sentence says: the guarded image of a sentence holds of k invented values exactly when the sentence holds in the instance, with the k copies of the block interpreted by the assignments those values mean.

The same at a single copy

theorem DescriptiveComplexity.readEquiv₁_rel {L Lt : FirstOrder.Language} {B : SOBlock} {S : ReadSyms L B Lt} {M A : Type} [Lt.Structure M] [L.IsRelational] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → B.Assignment A} (h : ReadOn S e means) (v : M) {n : ℕ} (r : ((L.sum FirstOrder.Language.order).sum B.lang).Relations n) (x : Fin n → A) : FirstOrder.Language.Structure.RelMap r x ↔ FirstOrder.Language.Structure.RelMap r x

The single-copy reading of DescriptiveComplexity.readEquiv_rel.

def DescriptiveComplexity.readEquiv₁ {L Lt : FirstOrder.Language} {B : SOBlock} {S : ReadSyms L B Lt} {M A : Type} [Lt.Structure M] [L.IsRelational] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → B.Assignment A} (h : ReadOn S e means) (v : M) : ((L.sum FirstOrder.Language.order).sum B.lang).Equiv A A

The single-copy reading of DescriptiveComplexity.readEquiv.

Equations

• DescriptiveComplexity.readEquiv₁ h v = { toEquiv := Equiv.refl A, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.realize_readHom₁ {L Lt : FirstOrder.Language} {B : SOBlock} {S : ReadSyms L B Lt} {M A : Type} [Lt.Structure M] [L.IsRelational] [L.Structure A] [LinearOrder A] {e : A → M} {means : M → B.Assignment A} (h : ReadOn S e means) {R : Lt.Relations 1} (hinj : Function.Injective e) (hR : ∀ (x : M), FirstOrder.Language.Structure.RelMap R ![x] ↔ ∃ (a : A), e a = x) (v : M) (φ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : (((readHom₁ S).relOnSentenceF R φ).Realize fun (x : Unit) => v) ↔ A ⊨ φ

The single-copy reading of DescriptiveComplexity.realize_readHom: the guarded image of a domain sentence holds of an invented value exactly when the sentence holds in the instance, the block interpreted by the assignment that value means.