A bounded extension lives inside the instance's own tuples

DescriptiveComplexity.SigmaSONewBddDefinable guesses an extension A ⊕ Fin m with m ≤ Nat.card (Fin d → A). That bound is exactly what it takes for the extension to be definable inside A: there are as many invented values as d-tuples, so the invented values can be taken to be d-tuples, guessed as one d-ary relation.

This file builds the interpretation that says so, in the shape DescriptiveComplexity.SecondOrderNewPull established for the other direction:

• two tags, false for the original elements and true for the invented ones, and dimension d;
• an original element is a diagonal tuple – so that each one is a single point, which is why the dimension has to be positive;
• an invented value is a tuple the guessed relation N holds of – so their number is Nat.card {v // N v}, which is at most Nat.card (Fin d → A) whatever N is, and reaches every value below it for a suitable N.

The defining formulas say the rest: a relation of the base vocabulary holds of interpreted points when they are all original and it holds of the elements on their diagonals; old marks the false-tagged points; and a relation variable of the guessed block is read off the pulled variable selected by the tags, as in DescriptiveComplexity.SOBlock.pull.

What comes out is DescriptiveComplexity.sorealize_bddPull – the kernel holds over some bounded extension exactly when its pullback holds over the instance – and from it DescriptiveComplexity.sigmaSONewBddDefinable_iff_sigmaSODefinable: ∃SO[new, d] = NP. Read beside DescriptiveComplexity.SecondOrderNewPull, which pulls the unbounded logic through an interpretation without ever eliminating the invention, this is what the bound is for: an interpretation cannot invent, so the values have to come from the instance, and the bound is exactly the promise that they can.

The guessed block

@[reducible, inline]

abbrev DescriptiveComplexity.bddBlock (d : ℕ) (B : SOBlock) : SOBlock

The block guessed on the instance: the set of invented values, as a d-ary relation, together with the pullback of the kernel's block through the two-tag interpretation.

Equations

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

def DescriptiveComplexity.newSetSym (d : ℕ) (B : SOBlock) : (bddBlock d B).lang.Relations d

The invented-values variable of the guessed block.

Equations

• DescriptiveComplexity.newSetSym d B = ⟨Sum.inl (), ⋯⟩

def DescriptiveComplexity.bddPullSym (d : ℕ) (B : SOBlock) {k : ℕ} (r : B.lang.Relations k) (τ : Fin k → Bool) : (bddBlock d B).lang.Relations (B.arity ↑r * d)

The pulled relation variable selected by a tuple of tags.

Equations

• DescriptiveComplexity.bddPullSym d B r τ = ⟨Sum.inr ⟨↑r, fun (j : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ j)⟩, ⋯⟩

The two vocabularies

@[reducible, inline]

abbrev DescriptiveComplexity.bddHost (L : FirstOrder.Language) (d : ℕ) (B : SOBlock) : FirstOrder.Language

The vocabulary the pulled-back kernel is written in: the instance's own, together with the guessed relation variables.

Equations

• DescriptiveComplexity.bddHost L d B = L.sum (DescriptiveComplexity.bddBlock d B).lang

@[reducible, inline]

abbrev DescriptiveComplexity.bddTarget (L : FirstOrder.Language) (B : SOBlock) : FirstOrder.Language

The vocabulary the kernel is written in: the extended vocabulary together with the block's relation variables.

Equations

• DescriptiveComplexity.bddTarget L B = (DescriptiveComplexity.newLang L).sum B.lang

The interpretation

@[reducible, inline]

abbrev DescriptiveComplexity.newSetHostSym (L : FirstOrder.Language) (d : ℕ) (B : SOBlock) : (bddHost L d B).Relations d

The invented-values variable, as a symbol of the host vocabulary.

Equations

• DescriptiveComplexity.newSetHostSym L d B = Sum.inr (DescriptiveComplexity.newSetSym d B)

@[reducible, inline]

abbrev DescriptiveComplexity.bddBlockHostSym (L : FirstOrder.Language) (d : ℕ) (B : SOBlock) {k : ℕ} (r : B.lang.Relations k) (τ : Fin k → Bool) : (bddHost L d B).Relations (B.arity ↑r * d)

A pulled relation variable, as a symbol of the host vocabulary.

Equations

• DescriptiveComplexity.bddBlockHostSym L d B r τ = Sum.inr (DescriptiveComplexity.bddPullSym d B r τ)

noncomputable def DescriptiveComplexity.bddDom (L : FirstOrder.Language) (d : ℕ) [NeZero d] (B : SOBlock) : Bool → (bddHost L d B).Formula (Fin d)

The domain formula: an original point is a diagonal tuple, so that each element of the instance is one point; an invented point is a tuple the guessed relation holds of.

Equations

• DescriptiveComplexity.bddDom L d B false = FirstOrder.Language.Formula.iInf fun (j : Fin d) => (FirstOrder.Language.var j).equal (FirstOrder.Language.var 0)
• DescriptiveComplexity.bddDom L d B true = (DescriptiveComplexity.newSetHostSym L d B).formula fun (j : Fin d) => FirstOrder.Language.var j

noncomputable def DescriptiveComplexity.bddRelF (L : FirstOrder.Language) (d : ℕ) [NeZero d] (B : SOBlock) {k : ℕ} : (bddTarget L B).Relations k → (Fin k → Bool) → (bddHost L d B).Formula (Fin k × Fin d)

The defining formulas: a symbol of the instance's vocabulary holds of interpreted points exactly when they are all original and it holds of the elements their diagonals carry, and never of an invented point; old marks the original points; a relation variable of the block is read off the pulled variable selected by the tags.

Equations

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

noncomputable def DescriptiveComplexity.bddInterp (L : FirstOrder.Language) (d : ℕ) [NeZero d] (B : SOBlock) : RelFOInterpretation (bddHost L d B) (bddTarget L B) Bool d

The extended universe, interpreted in the instance: two tags and dimension d, the original elements on the diagonal and the invented values wherever the guessed relation puts them.

Equations

• DescriptiveComplexity.bddInterp L d B = { relFormula := fun {n : ℕ} => DescriptiveComplexity.bddRelF L d B, domFormula := DescriptiveComplexity.bddDom L d B }

Realization in the host structure

def DescriptiveComplexity.newSet {A : Type} {d : ℕ} {B : SOBlock} (ρ : (bddBlock d B).Assignment A) : (Fin d → A) → Prop

The invented values, as the instance's own tuples: the d-tuples the guessed variable holds of. Their number is what the bound of DescriptiveComplexity.SigmaSONewBddDefinable allows.

Equations

• DescriptiveComplexity.newSet ρ v = ρ (Sum.inl ()) v

@[instance_reducible]

noncomputable def DescriptiveComplexity.bddHostStruc {L : FirstOrder.Language} {d : ℕ} {B : SOBlock} (A : Type) [L.Structure A] (ρ : (bddBlock d B).Assignment A) : (bddHost L d B).Structure A

The host structure: the instance, expanded by the guessed relation variables.

Equations

• DescriptiveComplexity.bddHostStruc A ρ = L.sumStructure (DescriptiveComplexity.bddBlock d B).lang A

theorem DescriptiveComplexity.realize_bddDom_false {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] {ρ : (bddBlock d B).Assignment A} (w : Fin d → A) : (bddDom L d B false).Realize w ↔ ∀ (j : Fin d), w j = w 0

theorem DescriptiveComplexity.realize_bddDom_true {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] {ρ : (bddBlock d B).Assignment A} (w : Fin d → A) : (bddDom L d B true).Realize w ↔ newSet ρ w

The extended universe as tagged tuples

def DescriptiveComplexity.bddPoint {d : ℕ} {A : Type} {m : ℕ} (e : Fin m → Fin d → A) : A ⊕ Fin m → Bool × (Fin d → A)

The tagged tuple representing a point of the extended universe: an original element on its diagonal, an invented value where the embedding puts it.

Equations

• DescriptiveComplexity.bddPoint e (Sum.inl a) = (false, fun (x : Fin d) => a)
• DescriptiveComplexity.bddPoint e (Sum.inr i) = (true, e i)

@[simp]

theorem DescriptiveComplexity.bddPoint_inl {d : ℕ} {A : Type} {m : ℕ} (e : Fin m → Fin d → A) (a : A) : bddPoint e (Sum.inl a) = (false, fun (x : Fin d) => a)

@[simp]

theorem DescriptiveComplexity.bddPoint_inr {d : ℕ} {A : Type} {m : ℕ} (e : Fin m → Fin d → A) (i : Fin m) : bddPoint e (Sum.inr i) = (true, e i)

theorem DescriptiveComplexity.bddPoint_injective {d : ℕ} [NeZero d] {A : Type} {m : ℕ} {e : Fin m → Fin d → A} (he : Function.Injective e) : Function.Injective (bddPoint e)

theorem DescriptiveComplexity.bddPoint_mem_dom {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (bddBlock d B).Assignment A) {e : Fin m → Fin d → A} (he : ∀ (i : Fin m), newSet ρ (e i)) (x : A ⊕ Fin m) : (bddDom L d B (bddPoint e x).1).Realize (bddPoint e x).2

theorem DescriptiveComplexity.bddPoint_surjective {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (bddBlock d B).Assignment A) {e : Fin m → Fin d → A} (hN : ∀ (v : Fin d → A), newSet ρ v ↔ ∃ (i : Fin m), e i = v) (t : Bool) (w : Fin d → A) : (bddDom L d B t).Realize w → ∃ (x : A ⊕ Fin m), bddPoint e x = (t, w)

def DescriptiveComplexity.bddTargetAssign {d : ℕ} {B : SOBlock} {A : Type} {m : ℕ} (e : Fin m → Fin d → A) (ρ : (bddBlock d B).Assignment A) : B.Assignment (A ⊕ Fin m)

The assignment of the kernel's block on the extended universe, read off a guessed assignment on the instance: the pulled variable selected by the tags of the arguments, at their coordinates.

Equations

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

The defining formulas, realized

theorem DescriptiveComplexity.realize_bddRelF_base {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] (ρ : (bddBlock d B).Assignment A) {k : ℕ} (R : L.Relations k) (a : Fin k → A) (w : Fin k × Fin d → A) (hw : ∀ (i : Fin k) (j : Fin d), w (i, j) = a i) : (bddRelF L d B (Sum.inl (Sum.inl R)) fun (x : Fin k) => false).Realize w ↔ FirstOrder.Language.Structure.RelMap R a

A base symbol at original points: the relation of the instance, at the elements the diagonals carry.

theorem DescriptiveComplexity.bddRelF_base_eq_bot {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {k : ℕ} (R : L.Relations k) (τ : Fin k → Bool) (h : ¬∀ (i : Fin k), τ i = false) : bddRelF L d B (Sum.inl (Sum.inl R)) τ = ⊥

A base symbol never holds of an invented point.

theorem DescriptiveComplexity.realize_bddRelF_old {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] (ρ : (bddBlock d B).Assignment A) (τ : Fin 1 → Bool) (w : Fin 1 × Fin d → A) : (bddRelF L d B (Sum.inl (Sum.inr FirstOrder.Language.oldRel.old)) τ).Realize w ↔ τ 0 = false

The marker old holds exactly of the original points.

theorem DescriptiveComplexity.realize_bddRelF_block {L : FirstOrder.Language} {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] (ρ : (bddBlock d B).Assignment A) {k : ℕ} (r : B.lang.Relations k) (τ : Fin k → Bool) (w : Fin k × Fin d → A) : (bddRelF L d B (Sum.inr r) τ).Realize w ↔ ρ (Sum.inr ⟨↑r, fun (j : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ j)⟩) fun (mm : Fin ((bddBlock d B).arity (Sum.inr ⟨↑r, fun (j : Fin (B.arity ↑r)) => τ (Fin.cast ⋯ j)⟩))) => w (Fin.cast ⋯ (finProdFinEquiv.symm mm).1, (finProdFinEquiv.symm mm).2)

A relation variable of the block is read off the pulled variable selected by the tags.

The interpreted universe is the extended universe

noncomputable def DescriptiveComplexity.bddTargetEquiv {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (e : Fin m → Fin d → A) (he : Function.Injective e) (ρ : (bddBlock d B).Assignment A) (hN : ∀ (v : Fin d → A), newSet ρ v ↔ ∃ (i : Fin m), e i = v) : (bddTarget L B).Equiv (A ⊕ Fin m) ((bddInterp L d B).MapRel A)

The interpreted structure is the extended structure: the map sending a point of A ⊕ Fin m to its tagged tuple is an isomorphism over the extended vocabulary, the block being interpreted by DescriptiveComplexity.bddTargetAssign.

Equations

• DescriptiveComplexity.bddTargetEquiv e he ρ hN = { toEquiv := Equiv.ofBijective (fun (x : A ⊕ Fin m) => ⟨DescriptiveComplexity.bddPoint e x, ⋯⟩) ⋯, map_fun' := ⋯, map_rel' := ⋯ }

The guess, read back

noncomputable def DescriptiveComplexity.bddBack {d : ℕ} [NeZero d] {A : Type} {m : ℕ} (e : Fin m → Fin d → A) : Bool → (Fin d → A) → A ⊕ Fin m

The point a tag and a tuple name: an original element on a diagonal, the invented value the embedding puts there. Off the embedding's image the value is junk, which no formula reaches – the domain formula rules those tuples out.

Equations

• DescriptiveComplexity.bddBack e false x✝ = Sum.inl (x✝ 0)
• DescriptiveComplexity.bddBack e true x✝ = if h : ∃ (i : Fin m), e i = x✝ then Sum.inr h.choose else Sum.inl (x✝ 0)

theorem DescriptiveComplexity.bddBack_bddPoint {d : ℕ} [NeZero d] {A : Type} {m : ℕ} {e : Fin m → Fin d → A} (he : Function.Injective e) (x : A ⊕ Fin m) : bddBack e (bddPoint e x).1 (bddPoint e x).2 = x

noncomputable def DescriptiveComplexity.bddSourceAssign {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} {m : ℕ} (e : Fin m → Fin d → A) (σ : B.Assignment (A ⊕ Fin m)) : (bddBlock d B).Assignment A

The guessed assignment on the instance, read off an assignment on the extended universe: the invented values are the embedding's image, and a pulled variable holds where the original one holds of the points its tags and coordinates name.

Equations

• DescriptiveComplexity.bddSourceAssign e σ (Sum.inl val) v = ∃ (i : Fin m), e i = v
• DescriptiveComplexity.bddSourceAssign e σ (Sum.inr p) x_2 = σ p.fst fun (k : Fin (B.arity p.fst)) => DescriptiveComplexity.bddBack e (p.snd k) fun (j : Fin d) => x_2 (finProdFinEquiv (k, j))

theorem DescriptiveComplexity.newSet_bddSourceAssign {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} {m : ℕ} (e : Fin m → Fin d → A) (σ : B.Assignment (A ⊕ Fin m)) (v : Fin d → A) : newSet (bddSourceAssign e σ) v ↔ ∃ (i : Fin m), e i = v

theorem DescriptiveComplexity.bddTargetAssign_bddSourceAssign {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} {m : ℕ} {e : Fin m → Fin d → A} (he : Function.Injective e) (σ : B.Assignment (A ⊕ Fin m)) : bddTargetAssign e (bddSourceAssign e σ) = σ

The two assignment transfers are inverse, in the direction an existential block needs: what the instance guesses is read back as what was guessed on the extended universe.

The kernel, pulled onto the instance

theorem DescriptiveComplexity.realize_bddTransfer {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} [NeZero d] {B : SOBlock} {A : Type} [L.Structure A] {m : ℕ} {e : Fin m → Fin d → A} (he : Function.Injective e) (ρ : (bddBlock d B).Assignment A) (hN : ∀ (v : Fin d → A), newSet ρ v ↔ ∃ (i : Fin m), e i = v) (σ : B.Assignment (A ⊕ Fin m)) (hσ : bddTargetAssign e ρ = σ) (φ : (bddTarget L B).Sentence) : (A ⊕ Fin m) ⊨ φ ↔ (bddInterp L d B).MapRel A ⊨ φ

Sentence transfer: what the kernel says in the extended universe, it says in the interpreted one.

theorem DescriptiveComplexity.sorealize_bddPull {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} [NeZero d] {B : SOBlock} (φ : (bddTarget L B).Sentence) (A : Type) [L.Structure A] [Finite A] : (∃ m ≤ Nat.card (Fin d → A), SORealize (newLang L) (A ⊕ Fin m) [B] φ true) ↔ SORealize L A [bddBlock d B] ((bddInterp L d B).pullRelSentence φ) true

A bounded extension is a guess on the instance: the kernel holds in A ⊕ Fin m for some m below the number of d-tuples exactly when its pullback through DescriptiveComplexity.bddInterp holds in A itself. The bound is what makes the forward direction possible – there have to be enough tuples to embed the invented values in – and the guessed relation is what makes the backward one, every d-ary relation cutting out at most that many.

theorem DescriptiveComplexity.SigmaSONewBddDefinable.toSigmaSO {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} [NeZero d] {P : DecisionProblem L} (h : SigmaSONewBddDefinable d P) : SigmaSODefinable 1 P

∃SO[new, d] ⊆ Σ₁: bounded value invention is existential second-order logic over the instance itself. The invented values are taken to be d-tuples, guessed as one more relation variable, and the kernel is pulled back through the two-tag interpretation. With DescriptiveComplexity.SigmaSODefinable.toNewBdd this is ∃SO[new, d] = NP.

theorem DescriptiveComplexity.sigmaSONewBddDefinable_iff_sigmaSODefinable {L : FirstOrder.Language} [L.IsRelational] {d : ℕ} [NeZero d] {P : DecisionProblem L} : SigmaSONewBddDefinable d P ↔ SigmaSODefinable 1 P

∃SO[new, d] = NP, for a positive dimension: bounding the invented values by the instance's d-tuples hands the search space back to the instance, which is what the parameter was for.