What an expansion atom's element loop computes

An atom r(p₁,…,p_k) of a step matrix is a relation of the expanded structure, so it holds exactly when the expansion's defining sentence X.relSentence r τ̄ – at the argument points' tags – holds of the base structure with one copy of the block per argument, interpreted by the points' assignments (DescriptiveComplexity.ExpExpansion.relMap_map). The machine evaluates that sentence by an element loop: its prefix is enumerated in the control's loop-variable slots, and per tuple its matrix is a Boolean function of atoms which are either guards – equalities, base relations, order on control-held elements, all evaluated by the transition table – or read leaves, one bit of one argument point's assignment (DescriptiveComplexity.Problems.Wide.DrawRepAtoms).

This file is the semantic anchor of that loop, the control-scale twin of DescriptiveComplexity.Problems.Wide.DrawLeaf: DescriptiveComplexity.Draw.Data.relMap_iff_altQuantFrom_expLeaf says the expanded relation is the prefix of DescriptiveComplexity.Draw.Data.expLeaf played from level 0, and the _pad variant says the same of the loop the machine actually runs, which enumerates every loop-variable slot – the levels past the sentence's own prefix being read by nobody (DescriptiveComplexity.Draw.altQuantFrom_pad).

The leaf of the loop

noncomputable def DescriptiveComplexity.Draw.Data.expLeaf {L : FirstOrder.Language} [L.IsRelational] (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (ρs : Fin k → dt.X.B.Assignment A) (u : Fin (dt.relPk e τ).n → A) : Prop

What one round of an expansion atom's element loop is worth: the Boolean value of the defining sentence's matrix at the control's tuple, its replicated-block atoms read off the argument points' assignments – one named bit each – and its base atoms decided by the guards.

Equations

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

The join

theorem DescriptiveComplexity.Draw.Data.relMap_iff_altQuantFrom_expLeaf {L : FirstOrder.Language} [L.IsRelational] (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {k : ℕ} (e : dt.X.E.Relations k) (p : Fin k → dt.X.Map A) (v : Fin (dt.relPk e fun (ℓ : Fin k) => (↑(p ℓ)).1).n → A) : FirstOrder.Language.Structure.RelMap e p ↔ altQuantFrom (dt.relPk e fun (ℓ : Fin k) => (↑(p ℓ)).1).pol (dt.expLeaf e (fun (ℓ : Fin k) => (↑(p ℓ)).1) fun (ℓ : Fin k) => (↑(p ℓ)).2) 0 v

The element loop computes the expanded relation. An atom of the expansion holds of a tuple of points exactly when the prefix of the leaf predicate, played from level 0, does – whatever the loop's slots held when it began, since level 0 reads no valuation.

theorem DescriptiveComplexity.Draw.Data.relMap_iff_altQuantFrom_expLeaf_pad {L : FirstOrder.Language} [L.IsRelational] (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] {k : ℕ} (e : dt.X.E.Relations k) (p : Fin k → dt.X.Map A) {N : ℕ} (hn : (dt.relPk e fun (ℓ : Fin k) => (↑(p ℓ)).1).n ≤ N) (t : Fin N → A) : FirstOrder.Language.Structure.RelMap e p ↔ altQuantFrom (dt.relPk e fun (ℓ : Fin k) => (↑(p ℓ)).1).pol (fun (w : Fin N → A) => dt.expLeaf e (fun (ℓ : Fin k) => (↑(p ℓ)).1) (fun (ℓ : Fin k) => (↑(p ℓ)).2) fun (j : Fin (dt.relPk e fun (ℓ : Fin k) => (↑(p ℓ)).1).n) => w (Fin.castLE hn j)) 0 t

The loop the machine runs, over every loop-variable slot: the levels past the sentence's own prefix are read by nobody, so playing them changes nothing.

The domain gate's sub-evaluation

The gate of a block value asks, after the shape checks, that the decoded assignment satisfy its tag's domain sentence – a sentence over the base vocabulary expanded by the block itself, not by a replicated one. The classifier being stated at an arbitrary block, it is the same element loop with one copy instead of k.

noncomputable def DescriptiveComplexity.Draw.Data.domLeaf {L : FirstOrder.Language} [L.IsRelational] (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] (t : dt.X.Tag) (ρ : dt.X.B.Assignment A) (u : Fin (dt.domPk t).n → A) : Prop

What one round of a domain gate's element loop is worth.

Equations

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

theorem DescriptiveComplexity.Draw.Data.domHolds_iff_altQuantFrom_domLeaf {L : FirstOrder.Language} [L.IsRelational] (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (t : dt.X.Tag) (ρ : dt.X.B.Assignment A) (v : Fin (dt.domPk t).n → A) : ExpExpansion.DomHolds (t, ρ) ↔ altQuantFrom (dt.domPk t).pol (dt.domLeaf t ρ) 0 v

The domain gate's loop computes the domain condition: a tagged assignment is a point of the expanded universe exactly when the prefix of its leaf predicate, played from level 0, holds.

theorem DescriptiveComplexity.Draw.Data.domHolds_iff_altQuantFrom_domLeaf_pad {L : FirstOrder.Language} [L.IsRelational] (dt : Data L) {A : Type} [L.Structure A] [LinearOrder A] [Nonempty A] (t : dt.X.Tag) (ρ : dt.X.B.Assignment A) {N : ℕ} (hn : (dt.domPk t).n ≤ N) (u : Fin N → A) : ExpExpansion.DomHolds (t, ρ) ↔ altQuantFrom (dt.domPk t).pol (fun (w : Fin N → A) => dt.domLeaf t ρ fun (j : Fin (dt.domPk t).n) => w (Fin.castLE hn j)) 0 u

The same over every loop-variable slot, which is what the machine's loop enumerates.