The expansion, relativized to the marked part

The doubled universe of DescriptiveComplexity.Problems.Wide.Double is never a singleton, which is what the machine needs, but it is no longer the instance. DescriptiveComplexity.Draw.relExp repairs that on the expansion's side: every sentence of the expansion is renamed and relativized to the mark, and every block assignment is required to be supported – to hold only of marked tuples – so that a point of the relativized expansion over the doubled universe is a point of the original expansion over the instance.

One tag is added. FirstOrder.Language.ExpExpansion requires its domain sentence to be satisfiable at every structure, including ones with no marked part at all, where a relativized sentence has nothing to be about; the tag none is the point that exists exactly there, and over a doubled universe – one that always has a marked part – it contributes nothing.

Two sentences about a structure with no marked part

noncomputable def DescriptiveComplexity.Draw.noOldSentence (L : FirstOrder.Language) (B : SOBlock) : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Sentence

No element is marked, as a sentence.

Equations

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

noncomputable def DescriptiveComplexity.Draw.emptyBlocksSentence (L : FirstOrder.Language) (B : SOBlock) : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Sentence

Every relation variable of the block is empty, as a sentence.

Equations

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

theorem DescriptiveComplexity.Draw.realize_noOldSentence {L : FirstOrder.Language} {B : SOBlock} {M : Type} [(newLang L).Structure M] [LinearOrder M] (ρ : B.Assignment M) : M ⊨ noOldSentence L B ↔ ∀ (x : M), ¬FirstOrder.Language.Structure.RelMap (oldNewSym L) ![x]

theorem DescriptiveComplexity.Draw.realize_emptyBlocksSentence {L : FirstOrder.Language} {B : SOBlock} {M : Type} [(newLang L).Structure M] [LinearOrder M] (ρ : B.Assignment M) : M ⊨ emptyBlocksSentence L B ↔ ∀ (i : B.ι) (w : Fin (B.arity i) → M), ¬ρ i w

The relativized expansion

noncomputable def DescriptiveComplexity.Draw.relExp {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) : ExpExpansion (newLang L)

The expansion, relativized to the marked part: the same block and the same expanded vocabulary, every sentence renamed and relativized, every assignment required to be supported, and one extra tag for the structures with no marked part.

Equations

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