Reading the instance inside the doubled universe

DescriptiveComplexity.Problems.Wide.Double runs the machinery at a universe that is never a singleton, at the price of a universe that is no longer the instance. This file pays that price for one sentence at a time: a sentence about the instance's ordered vocabulary, expanded by a block, is renamed into the extended vocabulary (DescriptiveComplexity.Draw.newBlockLHom) and relativized to the mark (DescriptiveComplexity.relativizeTo), and then says in the doubled universe exactly what it said in the instance (DescriptiveComplexity.Draw.realize_relOldBlock).

The block assignment travels with it. An assignment of the instance is extended to the doubled universe by DescriptiveComplexity.Draw.extAssign – it holds of a tuple exactly when every entry is marked and the entries' elements satisfy it – and that is the shape the support condition of the relativized expansion will pin down: an assignment over the doubled universe that only ever holds of marked tuples is an assignment of the instance and nothing more.

The lexicographic order, on the doubled universe

theorem DescriptiveComplexity.Draw.tupLeLex_one {A : Type} [LinearOrder A] (u v : Fin 1 → A) : tupLeLex u v ↔ u 0 ≤ v 0

On a one-coordinate tuple the lexicographic order is the order itself.

theorem DescriptiveComplexity.Draw.tagTupleLe_dblPt {A : Type} [LinearOrder A] {L : FirstOrder.Language} [L.IsRelational] [L.Structure A] (b : Bool) (a a' : A) : tagTupleLe (dblPt b a) (dblPt b a') ↔ a ≤ a'

Two points of the doubled universe with the same tag compare as their elements do.

The renaming, and the mark

def DescriptiveComplexity.Draw.newBlockLHom {L : FirstOrder.Language} [L.IsRelational] (B : SOBlock) : (L.sum FirstOrder.Language.order).sum B.lang →ᴸ ((newLang L).sum FirstOrder.Language.order).sum B.lang

Renaming a sentence about the instance – over its ordered vocabulary, expanded by a block – into the extended vocabulary.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.oldGuard {L : FirstOrder.Language} (B : SOBlock) : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Relations 1

The mark of the instance's own elements, in the block-expanded extended vocabulary.

Equations

• DescriptiveComplexity.Draw.oldGuard B = Sum.inl (Sum.inl (Sum.inr FirstOrder.Language.oldSym))

@[instance_reducible]

noncomputable instance DescriptiveComplexity.Draw.dblOrder {L : FirstOrder.Language} {A : Type} [LinearOrder A] : LinearOrder ((dblInterp L).Map A)

The order the reduction puts on the doubled universe: the instance's copy and the junk copy, each in the instance's order.

Equations

• DescriptiveComplexity.Draw.dblOrder = DescriptiveComplexity.tagTupleOrder

def DescriptiveComplexity.Draw.extAssign {L : FirstOrder.Language} {B : SOBlock} {A : Type} (ρ₀ : B.Assignment A) : B.Assignment ((dblInterp L).Map A)

An assignment of the instance, extended to the doubled universe: it holds of a tuple exactly when every entry is marked and the entries' elements satisfy it.

Equations

• DescriptiveComplexity.Draw.extAssign ρ₀ i w = ((∀ (j : Fin (B.arity i)), (w j).1 = false) ∧ ρ₀ i fun (j : Fin (B.arity i)) => (w j).2 0)

def DescriptiveComplexity.Draw.resAssign {L : FirstOrder.Language} {B : SOBlock} {A : Type} (ρ : B.Assignment ((dblInterp L).Map A)) : B.Assignment A

An assignment of the doubled universe, restricted to the instance.

Equations

• DescriptiveComplexity.Draw.resAssign ρ i w = ρ i fun (j : Fin (B.arity i)) => DescriptiveComplexity.Draw.dblPt false (w j)

@[simp]

theorem DescriptiveComplexity.Draw.resAssign_extAssign {L : FirstOrder.Language} {B : SOBlock} {A : Type} (ρ₀ : B.Assignment A) : resAssign (extAssign ρ₀) = ρ₀

def DescriptiveComplexity.Draw.Supported {L : FirstOrder.Language} {B : SOBlock} {A : Type} (ρ : B.Assignment ((dblInterp L).Map A)) : Prop

An assignment is supported when it only ever holds of marked tuples: the condition the relativized expansion pins down, and exactly what makes an assignment of the doubled universe an assignment of the instance.

Equations

• DescriptiveComplexity.Draw.Supported ρ = ∀ (i : B.ι) (w : Fin (B.arity i) → (DescriptiveComplexity.Draw.dblInterp L).Map A), ρ i w → ∀ (j : Fin (B.arity i)), (w j).1 = false

theorem DescriptiveComplexity.Draw.extAssign_resAssign {L : FirstOrder.Language} {B : SOBlock} {A : Type} {ρ : B.Assignment ((dblInterp L).Map A)} (h : Supported ρ) : extAssign (resAssign ρ) = ρ

The transport

The structures the transport is about are built from block assignments, so they are never instances: every statement below names them.

def DescriptiveComplexity.Draw.oldSubD (L : FirstOrder.Language) [L.IsRelational] (B : SOBlock) (A : Type) [L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Substructure ((dblInterp L).Map A)

The marked part of the doubled universe, as a substructure: the vocabulary is relational, so there is nothing to be closed under.

Equations

• DescriptiveComplexity.Draw.oldSubD L B A ρ₀ = { carrier := {p : (DescriptiveComplexity.Draw.dblInterp L).Map A | p.1 = false}, fun_mem := ⋯ }

noncomputable def DescriptiveComplexity.Draw.oldSubDEquiv {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) : A ≃ ↥(oldSubD L B A ρ₀)

The marked part is the instance: an element and its marked copy.

Equations

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

noncomputable def DescriptiveComplexity.Draw.oldSubDLEquiv {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) : ((L.sum FirstOrder.Language.order).sum B.lang).Equiv A ↥(oldSubD L B A ρ₀)

The marked part carries the instance, over the instance's own ordered vocabulary expanded by the block: an isomorphism, the reduct of the induced structure along the renaming being what the extended assignment restricts to.

Equations

• DescriptiveComplexity.Draw.oldSubDLEquiv ρ₀ = { toEquiv := DescriptiveComplexity.Draw.oldSubDEquiv ρ₀, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.Draw.realize_relOldBlock {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] (ρ₀ : B.Assignment A) (σ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : (dblInterp L).Map A ⊨ relativizeTo (oldGuard B) ((newBlockLHom B).onSentence σ) ↔ A ⊨ σ

Reading a sentence about the instance inside the doubled universe: its renaming, relativized to the mark, says of the extended assignment exactly what it said of the assignment.

The support condition, as a sentence

An assignment of the doubled universe is an assignment of the instance exactly when it never holds of an unmarked entry. That is one sentence per relation variable of the block, and it is the conjunct the relativized expansion's domain sentence carries beside the relativized original.

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.blkSym (L : FirstOrder.Language) (B : SOBlock) (i : B.ι) : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Relations (B.arity i)

A relation variable of the block, as a symbol of the expanded extended vocabulary: named, because a raw Sum.inr is not recognized at the transparency rw matches at.

Equations

• DescriptiveComplexity.Draw.blkSym L B i = Sum.inr ⟨i, ⋯⟩

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

One relation variable holds only of marked tuples, as a sentence.

Equations

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

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

The support condition, as a sentence: every relation variable of the block holds only of marked tuples.

Equations

• DescriptiveComplexity.Draw.suppSentence L B = DescriptiveComplexity.listInf (List.map (DescriptiveComplexity.Draw.suppAt L B) Finset.univ.toList)

The marked part of an arbitrary extended structure

The doubled universe is not the only structure the relativized expansion will be read at: FirstOrder.Language.ExpExpansion demands its domain sentence be satisfiable at every structure, so the marked part has to be an instance in its own right wherever there is one.

def DescriptiveComplexity.Draw.MarkPart (L : FirstOrder.Language) [L.IsRelational] (M : Type) [(newLang L).Structure M] : Type

The marked part of an extended structure. A def, so that its instances below are found by their own head rather than by the subtype's.

Equations

• DescriptiveComplexity.Draw.MarkPart L M = { x : M // FirstOrder.Language.Structure.RelMap (DescriptiveComplexity.Draw.oldNewSym L) ![x] }

def DescriptiveComplexity.Draw.MarkPart.val {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (x : MarkPart L M) : M

The element a marked point is.

Equations

• x.val = ↑x

theorem DescriptiveComplexity.Draw.MarkPart.isMark {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (x : MarkPart L M) : FirstOrder.Language.Structure.RelMap (oldNewSym L) ![x.val]

theorem DescriptiveComplexity.Draw.MarkPart.ext {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] {x y : MarkPart L M} (h : x.val = y.val) : x = y

def DescriptiveComplexity.Draw.MarkPart.mk {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (x : M) (h : FirstOrder.Language.Structure.RelMap (oldNewSym L) ![x]) : MarkPart L M

A marked element, as a point of the marked part.

Equations

• DescriptiveComplexity.Draw.MarkPart.mk x h = ⟨x, h⟩

@[simp]

theorem DescriptiveComplexity.Draw.MarkPart.val_mk {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (x : M) (h : FirstOrder.Language.Structure.RelMap (oldNewSym L) ![x]) : (mk x h).val = x

@[instance_reducible]

instance DescriptiveComplexity.Draw.instLinearOrderMarkPart {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] [LinearOrder M] : LinearOrder (MarkPart L M)

Equations

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

instance DescriptiveComplexity.Draw.instFiniteMarkPart {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] [Finite M] : Finite (MarkPart L M)

@[instance_reducible]

instance DescriptiveComplexity.Draw.markStructure {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] : L.Structure (MarkPart L M)

The instance's own relations, on its marked part.

Equations

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

def DescriptiveComplexity.Draw.extAssignM {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (B : SOBlock) (ρ₀ : B.Assignment (MarkPart L M)) : B.Assignment M

An assignment of the marked part, extended to the whole structure: it holds of a tuple exactly when every entry is marked and the marked entries satisfy it.

Equations

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

def DescriptiveComplexity.Draw.markSub {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (B : SOBlock) [LinearOrder M] (ρ : B.Assignment M) : (((newLang L).sum FirstOrder.Language.order).sum B.lang).Substructure M

The marked part, as a substructure of the block-expanded extended vocabulary.

Equations

• DescriptiveComplexity.Draw.markSub B ρ = { carrier := {x : M | FirstOrder.Language.Structure.RelMap (DescriptiveComplexity.Draw.oldNewSym L) ![x]}, fun_mem := ⋯ }

noncomputable def DescriptiveComplexity.Draw.markSubLEquiv {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (B : SOBlock) [LinearOrder M] (ρ₀ : B.Assignment (MarkPart L M)) : ((L.sum FirstOrder.Language.order).sum B.lang).Equiv (MarkPart L M) ↥(markSub B (extAssignM B ρ₀))

The marked part carries the instance it marks: the identity map is an isomorphism from the marked part, with the structures above, onto the substructure with the reduct of its induced structure.

Equations

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

theorem DescriptiveComplexity.Draw.realize_relOldMark {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (B : SOBlock) [LinearOrder M] (ρ₀ : B.Assignment (MarkPart L M)) (σ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : M ⊨ relativizeTo (oldGuard B) ((newBlockLHom B).onSentence σ) ↔ MarkPart L M ⊨ σ

Reading a sentence about the marked part inside the structure: its renaming, relativized to the mark, says of the extended assignment exactly what it said of the assignment.

theorem DescriptiveComplexity.Draw.supported_extAssignM {L : FirstOrder.Language} [L.IsRelational] {M : Type} [(newLang L).Structure M] (B : SOBlock) (ρ₀ : B.Assignment (MarkPart L M)) (i : B.ι) (w : Fin (B.arity i) → M) : extAssignM B ρ₀ i w → ∀ (j : Fin (B.arity i)), FirstOrder.Language.Structure.RelMap (oldNewSym L) ![w j]

An extended assignment is supported: nothing but marked tuples.

theorem DescriptiveComplexity.Draw.realize_suppAt {L : FirstOrder.Language} {M : Type} [(newLang L).Structure M] (B : SOBlock) [LinearOrder M] (ρ : B.Assignment M) (i : B.ι) : M ⊨ suppAt L B i ↔ ∀ (w : Fin (B.arity i) → M), ρ i w → ∀ (j : Fin (B.arity i)), FirstOrder.Language.Structure.RelMap (oldNewSym L) ![w j]

The support condition, read: an assignment satisfies the support sentence exactly when it never holds of an unmarked entry.

theorem DescriptiveComplexity.Draw.realize_suppSentence {L : FirstOrder.Language} {M : Type} [(newLang L).Structure M] (B : SOBlock) [LinearOrder M] (ρ : B.Assignment M) : M ⊨ suppSentence L B ↔ ∀ (i : B.ι) (w : Fin (B.arity i) → M), ρ i w → ∀ (j : Fin (B.arity i)), FirstOrder.Language.Structure.RelMap (oldNewSym L) ![w j]