The expansion a bounded invention lives in

DescriptiveComplexity.SigmaSONewExpDefinable guesses an extension A ⊕ Fin m with m ≤ 2 ^ Nat.card (Fin d → A) – as many invented values as the instance has d-ary relations. To read such a definition as one over an exponential expansion, the expansion has to be big enough to hold them, and it has to carry the instance too, since an expansion is all a sentence over it can see.

This file builds that expansion. It has two tags:

• an original point is an assignment whose unary variable is a singleton and whose d-ary one is empty – so those points are the elements of the instance;
• a new point is an assignment whose unary variable is empty – so those points are the d-ary relations of the instance, 2 ^ nᵈ of them.

Its vocabulary is DescriptiveComplexity.newLang L: the relations of the instance, holding of original points exactly where they hold of the elements they name, and the marker old. What the expanded structure is, then, is the extended structure A ⊕ Fin (2 ^ nᵈ) with every invented value present; a sentence that wants fewer of them marks the ones it uses, which is a guess and so stays inside Σ₁.

The block

@[reducible, inline]

abbrev DescriptiveComplexity.powBlock (c d : ℕ) : SOBlock

The block whose assignments are the points of the expansion: one d-ary variable carrying an invented value and one unary variable carrying an original element.

Equations

• DescriptiveComplexity.powBlock c d = { ι := Option (Fin c), ιFinite := ⋯, arity := fun (i : Option (Fin c)) => i.elim 1 fun (x : Fin c) => d }

def DescriptiveComplexity.powValSym (c d : ℕ) (i : Fin c) : (powBlock c d).lang.Relations d

The i-th d-ary variable: one coordinate of an invented value.

Equations

• DescriptiveComplexity.powValSym c d i = ⟨some i, ⋯⟩

def DescriptiveComplexity.powEltSym (c d : ℕ) : (powBlock c d).lang.Relations 1

The unary variable: an original element.

Equations

• DescriptiveComplexity.powEltSym c d = ⟨none, ⋯⟩

def DescriptiveComplexity.powEltSymAt (c d : ℕ) {n : ℕ} (k : Fin n) : ((powBlock c d).replicate n).lang.Relations 1

The unary variable of the k-th copy.

Equations

• DescriptiveComplexity.powEltSymAt c d k = (DescriptiveComplexity.powBlock c d).replicateSym k (DescriptiveComplexity.powEltSym c d)

The sentences

noncomputable def DescriptiveComplexity.eltAtom (L : FirstOrder.Language) (c d : ℕ) {α : Type} (x : α) : (L.sum (powBlock c d).lang).Formula α

The atom elt x, over the vocabulary of the block.

Equations

• DescriptiveComplexity.eltAtom L c d x = FirstOrder.Language.Relations.formula (Sum.inr (DescriptiveComplexity.powEltSym c d)) fun (x_1 : Fin 1) => FirstOrder.Language.var x

noncomputable def DescriptiveComplexity.eltAtomAt (L : FirstOrder.Language) (c d : ℕ) {n : ℕ} (k : Fin n) {α : Type} (x : α) : (L.sum ((powBlock c d).replicate n).lang).Formula α

The atom eltₖ x, over the vocabulary of n copies of the block.

Equations

• DescriptiveComplexity.eltAtomAt L c d k x = FirstOrder.Language.Relations.formula (Sum.inr (DescriptiveComplexity.powEltSymAt c d k)) fun (x_1 : Fin 1) => FirstOrder.Language.var x

noncomputable def DescriptiveComplexity.valAtom (L : FirstOrder.Language) (c d : ℕ) (i : Fin c) {α : Type} (w : Fin d → α) : (L.sum (powBlock c d).lang).Formula α

The atom valᵢ w, over the vocabulary of the block.

Equations

• DescriptiveComplexity.valAtom L c d i w = FirstOrder.Language.Relations.formula (Sum.inr (DescriptiveComplexity.powValSym c d i)) fun (j : Fin d) => FirstOrder.Language.var (w j)

noncomputable def DescriptiveComplexity.eltUnique (L : FirstOrder.Language) (c d : ℕ) : (L.sum (powBlock c d).lang).Sentence

elt holds of exactly one element.

Equations

• DescriptiveComplexity.eltUnique L c d = FirstOrder.Language.Formula.iExsUnique (Fin 1) (DescriptiveComplexity.eltAtom L c d (Sum.inr 0))

noncomputable def DescriptiveComplexity.eltEmpty (L : FirstOrder.Language) (c d : ℕ) : (L.sum (powBlock c d).lang).Sentence

elt holds of nothing.

Equations

• DescriptiveComplexity.eltEmpty L c d = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.eltAtom L c d (Sum.inr 0)))

noncomputable def DescriptiveComplexity.valEmpty (L : FirstOrder.Language) (c d : ℕ) : (L.sum (powBlock c d).lang).Sentence

No coordinate of the invented value holds of anything.

Equations

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

noncomputable def DescriptiveComplexity.powDom (L : FirstOrder.Language) (c d : ℕ) : Bool → (L.sum (powBlock c d).lang).Sentence

The domain sentence of each tag: an original point names one element and invents nothing; a new point names no element.

Equations

• DescriptiveComplexity.powDom L c d false = DescriptiveComplexity.eltUnique L c d ⊓ DescriptiveComplexity.valEmpty L c d
• DescriptiveComplexity.powDom L c d true = DescriptiveComplexity.eltEmpty L c d

noncomputable def DescriptiveComplexity.powRelSentence (L : FirstOrder.Language) (c d : ℕ) {n : ℕ} : (newLang L).Relations n → (Fin n → Bool) → (L.sum ((powBlock c d).replicate n).lang).Sentence

The defining sentence of each symbol: a relation of the instance holds of original points exactly when it holds of the elements they name, and never of a new point; old marks the original points.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.powRelSentence L c d (Sum.inr FirstOrder.Language.oldRel.old) τ_1 = if τ_1 0 = false then ⊤ else ⊥

The sentences, realized

def DescriptiveComplexity.eltOf {c d : ℕ} {A : Type} (ρ : (powBlock c d).Assignment A) : A → Prop

The unary variable, read off the assignment.

Equations

• DescriptiveComplexity.eltOf ρ x = ρ none fun (x_1 : Fin ((DescriptiveComplexity.powBlock c d).arity none)) => x

def DescriptiveComplexity.valOf {c d : ℕ} {A : Type} (ρ : (powBlock c d).Assignment A) : Fin c → (Fin d → A) → Prop

The d-ary variables, read off the assignment.

Equations

• DescriptiveComplexity.valOf ρ i w = ρ (some i) w

theorem DescriptiveComplexity.realize_eltEmpty {L : FirstOrder.Language} {c d : ℕ} {A : Type} [L.Structure A] (ρ : (powBlock c d).Assignment A) : A ⊨ eltEmpty L c d ↔ ∀ (x : A), ¬eltOf ρ x

The expansion

@[reducible]

noncomputable def DescriptiveComplexity.powExpFree (L : FirstOrder.Language) [L.IsRelational] (c d : ℕ) : ExpExpansionFree L

The expansion: two tags, the instance's elements and its d-ary relations, over the extended vocabulary.

Reducible: its block and its vocabulary have to reduce for instance search, or the structure a domain sentence is read in is not the one the realization lemmas are stated at.

Equations

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

The points of the expansion

instance DescriptiveComplexity.instNonemptyFinArityPowBlockNone {c d : ℕ} : Nonempty (Fin ((powBlock c d).arity none))

def DescriptiveComplexity.eltAssign {c d : ℕ} {A : Type} (x : A) : (powBlock c d).Assignment A

The assignment naming an original element: its unary variable holds of that element alone, and it invents nothing.

Equations

• DescriptiveComplexity.eltAssign x none u = ∀ (j : Fin ((DescriptiveComplexity.powBlock c d).arity none)), u j = x
• DescriptiveComplexity.eltAssign x (some val) x_3 = False

def DescriptiveComplexity.valAssign {c d : ℕ} {A : Type} (S : Fin c → (Fin d → A) → Prop) : (powBlock c d).Assignment A

The assignment naming an invented value: its unary variable holds of nothing, and its d-ary ones are the value's coordinates.

Equations

• DescriptiveComplexity.valAssign S none u = False
• DescriptiveComplexity.valAssign S (some val) x_2 = S val x_2

@[simp]

theorem DescriptiveComplexity.eltOf_eltAssign {c d : ℕ} {A : Type} (x y : A) : eltOf (eltAssign x) y ↔ y = x

@[simp]

theorem DescriptiveComplexity.valOf_eltAssign {c d : ℕ} {A : Type} (x : A) (i : Fin c) (w : Fin d → A) : ¬valOf (eltAssign x) i w

@[simp]

theorem DescriptiveComplexity.eltOf_valAssign {c d : ℕ} {A : Type} (S : Fin c → (Fin d → A) → Prop) (y : A) : ¬eltOf (valAssign S) y

@[simp]

theorem DescriptiveComplexity.valOf_valAssign {c d : ℕ} {A : Type} (S : Fin c → (Fin d → A) → Prop) (i : Fin c) (w : Fin d → A) : valOf (valAssign S) i w ↔ S i w

theorem DescriptiveComplexity.domHolds_eltAssign {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] (x : A) : ExpExpansionFree.DomHolds (false, eltAssign x)

theorem DescriptiveComplexity.domHolds_valAssign {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] (S : Fin c → (Fin d → A) → Prop) : ExpExpansionFree.DomHolds (true, valAssign S)

The points, counted

instance DescriptiveComplexity.instSubsingletonFinArityPowBlockNone {c d : ℕ} : Subsingleton (Fin ((powBlock c d).arity none))

def DescriptiveComplexity.powPoint {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] : A ⊕ (Fin c → (Fin d → A) → Prop) → (powExpFree L c d).Map A

The point of the expansion carried by an element or by a tuple of d-ary relations.

Equations

• DescriptiveComplexity.powPoint (Sum.inl x_1) = ⟨(false, DescriptiveComplexity.eltAssign x_1), ⋯⟩
• DescriptiveComplexity.powPoint (Sum.inr S) = ⟨(true, DescriptiveComplexity.valAssign S), ⋯⟩

theorem DescriptiveComplexity.powPoint_injective {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] : Function.Injective powPoint

theorem DescriptiveComplexity.powPoint_surjective {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] : Function.Surjective powPoint

noncomputable def DescriptiveComplexity.powPointEquiv {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] : A ⊕ (Fin c → (Fin d → A) → Prop) ≃ (powExpFree L c d).Map A

The points of the expansion are the instance's elements and its d-ary relations, so there are n + 2 ^ nᵈ of them: enough to hold any extension the bound of DescriptiveComplexity.SigmaSONewExpDefinable allows.

Equations

• DescriptiveComplexity.powPointEquiv = Equiv.ofBijective DescriptiveComplexity.powPoint ⋯

The defining sentences, realized

theorem DescriptiveComplexity.realize_eltAtomAt {L : FirstOrder.Language} {c d n : ℕ} {A : Type} [L.Structure A] (ρs : Fin n → (powBlock c d).Assignment A) (k : Fin n) {α : Type} (x : α) (v : α → A) : (eltAtomAt L c d k x).Realize v ↔ eltOf (ρs k) (v x)

theorem DescriptiveComplexity.realize_powRelSentence_base {L : FirstOrder.Language} {c d n : ℕ} {A : Type} [L.Structure A] (ρs : Fin n → (powBlock c d).Assignment A) (R : L.Relations n) (τ : Fin n → Bool) (hτ : ∀ (i : Fin n), τ i = false) : A ⊨ powRelSentence L c d (Sum.inl R) τ ↔ ∃ (x : Fin n → A), (∀ (i : Fin n), eltOf (ρs i) (x i)) ∧ FirstOrder.Language.Structure.RelMap R x

A relation of the instance, at original points: it holds exactly when it holds of the elements they name.

theorem DescriptiveComplexity.powRelSentence_base_eq_bot {L : FirstOrder.Language} {c d n : ℕ} (R : L.Relations n) (τ : Fin n → Bool) (hτ : ¬∀ (i : Fin n), τ i = false) : powRelSentence L c d (Sum.inl R) τ = ⊥

A relation of the instance never holds of an invented point.

theorem DescriptiveComplexity.realize_powRelSentence_old {L : FirstOrder.Language} {c d : ℕ} {A : Type} [L.Structure A] (σs : Fin 1 → (powBlock c d).Assignment A) (τ : Fin 1 → Bool) : A ⊨ powRelSentence L c d (Sum.inr FirstOrder.Language.oldSym) τ ↔ τ 0 = false

The marker old holds exactly of the original points.

The expanded structure is the extended structure

@[instance_reducible]

def DescriptiveComplexity.extOn (L : FirstOrder.Language) [L.IsRelational] (A N : Type) [L.Structure A] : (newLang L).Structure (A ⊕ N)

The extended structure over an arbitrary set of invented values: the relations of the instance hold of original elements only, and old marks them. DescriptiveComplexity.extStructure is the case N = Fin m.

Equations

• DescriptiveComplexity.extOn L A N = L.sumStructure FirstOrder.Language.oldMark (A ⊕ N)

theorem DescriptiveComplexity.relMap_extOn_base {L : FirstOrder.Language} [L.IsRelational] {A : Type} [L.Structure A] {N : Type} {k : ℕ} (R : L.Relations k) (x : Fin k → A ⊕ N) : FirstOrder.Language.Structure.RelMap (Sum.inl R) x ↔ ∃ (y : Fin k → A), (∀ (i : Fin k), x i = Sum.inl (y i)) ∧ FirstOrder.Language.Structure.RelMap R y

theorem DescriptiveComplexity.relMap_extOn_old {L : FirstOrder.Language} [L.IsRelational] {A : Type} [L.Structure A] {N : Type} (x : Fin 1 → A ⊕ N) : FirstOrder.Language.Structure.RelMap (Sum.inr FirstOrder.Language.oldSym) x ↔ IsOld (x 0)

noncomputable def DescriptiveComplexity.powExtEquiv {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {A : Type} [L.Structure A] : (newLang L).Equiv (A ⊕ (Fin c → (Fin d → A) → Prop)) ((powExpFree L c d).Map A)

The expanded structure is the extended one: the map sending an element to its original point and a d-ary relation to its new point is an isomorphism over DescriptiveComplexity.newLang.

Equations

• DescriptiveComplexity.powExtEquiv = { toEquiv := DescriptiveComplexity.powPointEquiv, map_fun' := ⋯, map_rel' := ⋯ }

The marked part of an extended universe

def DescriptiveComplexity.usedSub {L : FirstOrder.Language} [L.IsRelational] {A N : Type} [L.Structure A] (U : N → Prop) : (newLang L).Substructure (A ⊕ N)

The original elements together with the marked invented values: a substructure, there being nothing to be closed under in a relational vocabulary.

Equations

• DescriptiveComplexity.usedSub U = { carrier := {x : A ⊕ N | Sum.elim (fun (x : A) => True) U x}, fun_mem := ⋯ }

def DescriptiveComplexity.usedPoint {A N : Type} (U : N → Prop) : A ⊕ { y : N // U y } → A ⊕ N

The inclusion of the extension by the marked values into the whole one.

Equations

• DescriptiveComplexity.usedPoint U = Sum.map id Subtype.val

theorem DescriptiveComplexity.usedPoint_mem {L : FirstOrder.Language} [L.IsRelational] {A N : Type} [L.Structure A] (U : N → Prop) (x : A ⊕ { y : N // U y }) : usedPoint U x ∈ usedSub U

theorem DescriptiveComplexity.usedPoint_isOld {A N : Type} (U : N → Prop) (x : A ⊕ { y : N // U y }) : IsOld (usedPoint U x) ↔ IsOld x

theorem DescriptiveComplexity.usedPoint_eq_inl {A N : Type} (U : N → Prop) (x : A ⊕ { y : N // U y }) (a : A) : usedPoint U x = Sum.inl a ↔ x = Sum.inl a

def DescriptiveComplexity.usedSubEquiv {L : FirstOrder.Language} [L.IsRelational] {A N : Type} [L.Structure A] (U : N → Prop) : (newLang L).Equiv (A ⊕ { y : N // U y }) ↥(usedSub U)

The marked part is the extended universe over the marked values: the invented values a sentence uses are the ones it marks, and what it says of them it says of the extension by those alone.

Equations

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

The sentence read over the expansion

@[reducible, inline]

abbrev DescriptiveComplexity.markerBlock : SOBlock

The unary marker a sentence over the expansion guesses: which invented values it uses.

Equations

• DescriptiveComplexity.markerBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 1 }

@[reducible, inline]

abbrev DescriptiveComplexity.usedBlock (B : SOBlock) : SOBlock

The block guessed over the expansion: the kernel's own variables together with the marker.

Equations

• DescriptiveComplexity.usedBlock B = B.cons DescriptiveComplexity.markerBlock

@[reducible, inline]

abbrev DescriptiveComplexity.markerSym (B : SOBlock) : (usedBlock B).lang.Relations 1

The marker, as a symbol of the guessed vocabulary.

Equations

• DescriptiveComplexity.markerSym B = ⟨Sum.inr (), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.markerHostSym (L : FirstOrder.Language) (B : SOBlock) : ((newLang L).sum (usedBlock B).lang).Relations 1

The marker, as a symbol over the extended vocabulary.

Equations

• DescriptiveComplexity.markerHostSym L B = Sum.inr (DescriptiveComplexity.markerSym B)

@[reducible, inline]

abbrev DescriptiveComplexity.oldUsedSym (L : FirstOrder.Language) (B : SOBlock) : ((newLang L).sum (usedBlock B).lang).Relations 1

old, as a symbol over the same vocabulary.

Equations

• DescriptiveComplexity.oldUsedSym L B = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

noncomputable def DescriptiveComplexity.oldMarked (L : FirstOrder.Language) (B : SOBlock) : ((newLang L).sum (usedBlock B).lang).Sentence

Every original element is marked: the guess adds invented values to the instance, it does not take elements away.

Equations

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

noncomputable def DescriptiveComplexity.usedKernelHom (L : FirstOrder.Language) (B : SOBlock) : (newLang L).sum B.lang →ᴸ (newLang L).sum (usedBlock B).lang

The kernel, transported into the merged block.

Equations

• DescriptiveComplexity.usedKernelHom L B = (DescriptiveComplexity.mergeStep (DescriptiveComplexity.newLang L) B DescriptiveComplexity.markerBlock).comp FirstOrder.Language.LHom.sumInl

noncomputable def DescriptiveComplexity.usedSentence (L : FirstOrder.Language) (B : SOBlock) (φ : ((newLang L).sum B.lang).Sentence) : ((newLang L).sum (usedBlock B).lang).Sentence

The sentence read over the expansion: mark the invented values it uses, mark every original element, and read the kernel among the marked ones.

Equations

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

The marked part, with the kernel's block

The sentence over the expansion, realized

def DescriptiveComplexity.usedExtend {A N : Type} {B : SOBlock} (U : N → Prop) (ρ : B.Assignment (A ⊕ { y : N // U y })) : B.Assignment (A ⊕ N)

The assignment on the whole extension reproducing one on the extension by the marked values: a tuple is related exactly when it is the image of a related tuple.

Equations

• DescriptiveComplexity.usedExtend U ρ i x = ∃ (z : Fin (B.arity i) → A ⊕ { y : N // U y }), (∀ (j : Fin (B.arity i)), DescriptiveComplexity.usedPoint U (z j) = x j) ∧ ρ i z

def DescriptiveComplexity.markerOf {A N : Type} {B : SOBlock} (ρ' : (usedBlock B).Assignment (A ⊕ N)) : A ⊕ N → Prop

The marker, read off a guessed assignment.

Equations

• DescriptiveComplexity.markerOf ρ' x = ρ' (Sum.inr ()) fun (x_1 : Fin ((DescriptiveComplexity.usedBlock B).arity (Sum.inr ()))) => x

instance DescriptiveComplexity.instSubsingletonFinArityUsedBlockInrιMarkerBlockUnit {B : SOBlock} : Subsingleton (Fin ((usedBlock B).arity (Sum.inr ())))

def DescriptiveComplexity.kernelOf {A N : Type} {B : SOBlock} (ρ' : (usedBlock B).Assignment (A ⊕ N)) : B.Assignment (A ⊕ N)

The kernel's part of a guessed assignment.

Equations

• DescriptiveComplexity.kernelOf ρ' i = ρ' (Sum.inl i)

def DescriptiveComplexity.usedJoin {A N : Type} {B : SOBlock} (U : N → Prop) (ρ : B.Assignment (A ⊕ { y : N // U y })) : (usedBlock B).Assignment (A ⊕ N)

A guessed assignment, from its two parts.

Equations

• DescriptiveComplexity.usedJoin U ρ (Sum.inl i) x_2 = DescriptiveComplexity.usedExtend U ρ i x_2
• DescriptiveComplexity.usedJoin U ρ (Sum.inr val) x_2 = Sum.elim (fun (x : A) => True) U (x_2 ⟨0, Nat.zero_lt_one⟩)

@[simp]

theorem DescriptiveComplexity.markOf_usedJoin {A N : Type} {B : SOBlock} (U : N → Prop) (ρ : B.Assignment (A ⊕ { y : N // U y })) (x : A ⊕ N) : markerOf (usedJoin U ρ) x ↔ Sum.elim (fun (x : A) => True) U x

@[simp]

theorem DescriptiveComplexity.blockOf_usedJoin {A N : Type} {B : SOBlock} (U : N → Prop) (ρ : B.Assignment (A ⊕ { y : N // U y })) : kernelOf (usedJoin U ρ) = usedExtend U ρ

Bounded invention is definability over the expansion

theorem DescriptiveComplexity.sumCongr_eq_inl {A N N' : Type} (e : N ≃ N') (x : A ⊕ N) (a : A) : ((Equiv.refl A).sumCongr e) x = Sum.inl a ↔ x = Sum.inl a

theorem DescriptiveComplexity.sumCongr_isOld {A N N' : Type} (e : N ≃ N') (x : A ⊕ N) : IsOld (((Equiv.refl A).sumCongr e) x) ↔ IsOld x

def DescriptiveComplexity.extOnCongr {L : FirstOrder.Language} [L.IsRelational] {A N N' : Type} [L.Structure A] (e : N ≃ N') : (newLang L).Equiv (A ⊕ N) (A ⊕ N')

Renaming the invented values: the extended structure depends on them only through their number.

Equations

• DescriptiveComplexity.extOnCongr e = { toEquiv := (Equiv.refl A).sumCongr e, map_fun' := ⋯, map_rel' := ⋯ }

def DescriptiveComplexity.usedProblem {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} (φ : ((newLang L).sum B.lang).Sentence) : DecisionProblem (newLang L)

The problem the expansion decides: the kernel, read over the extension by the invented values a guess marks.

Equations

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

theorem DescriptiveComplexity.usedProblem_mem_NP {L : FirstOrder.Language} [L.IsRelational] {B : SOBlock} (φ : ((newLang L).sum B.lang).Sentence) : NP.Mem (usedProblem φ)

theorem DescriptiveComplexity.SigmaSONewExpDefinable.toExpDefinable {L : FirstOrder.Language} [L.IsRelational] {c d : ℕ} {P : DecisionProblem L} (h : SigmaSONewExpDefinable c d P) : ExpDefinable NP P

Bounded invention is definability over the expansion: an ∃SO[new, exp c d] definition is an ∃SO definition over DescriptiveComplexity.powExpFree, which is ∃SO[new, exp c d] ⊆ NEXPTIME.