A base that is never a singleton

Every track of the EXPSPACE machine is an element of the base universe, so the whole construction needs two of them (DescriptiveComplexity.Draw.Env.hzo, DescriptiveComplexity.Draw.Table.zero_ne_one) – and a reduction has to be correct at one-element structures too. The fix is to run the machinery not at the instance but at a doubled universe, which is never a singleton, and which is an ordinary first-order interpretation of the instance so that nothing is lost:

• the universe is Bool × (Fin 1 → A), i.e., two copies of A;
• the copy tagged false carries the instance's own relations, and is marked by the old symbol of DescriptiveComplexity.newLang;
• the copy tagged true is junk: no relation of the vocabulary touches it.

So the doubled universe is the extended universe of value invention (DescriptiveComplexity.SecondOrderNew) with |A| invented values, and DescriptiveComplexity.relativizeTo is what reads a formula about the instance inside it. What the reduction then has to do – and what DescriptiveComplexity.Problems.Wide.RelExpansion does – is relativize the expansion the same way, so that its points are still the instance's.

The interpretation is plain (not relativized) and one-dimensional, so composing it under the wide interpretation multiplies the dimension by one and the tags by Bool ^ dd: the composite is again a tagged-tuple interpretation of the instance, with the same dimension.

The interpretation

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.newSym {L : FirstOrder.Language} {n : ℕ} (r : L.Relations n) : (newLang L).Relations n

A relation of the instance's vocabulary, inside the extended one: named, because a raw Sum.inl is not recognized at the transparency rw matches at.

Equations

• DescriptiveComplexity.Draw.newSym r = Sum.inl r

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.oldNewSym (L : FirstOrder.Language) : (newLang L).Relations 1

The mark of the original elements, named for the same reason.

Equations

• DescriptiveComplexity.Draw.oldNewSym L = Sum.inr FirstOrder.Language.oldSym

noncomputable def DescriptiveComplexity.Draw.dblInterp (L : FirstOrder.Language) : FOInterpretation (L.sum FirstOrder.Language.order) (newLang L) Bool 1

The doubled universe, as an interpretation: the false copy carries the instance and is marked old, the true copy is junk.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Draw.dblPt {L : FirstOrder.Language} {A : Type} (b : Bool) (a : A) : (dblInterp L).Map A

The point of the doubled universe carried by a tag and an element.

Equations

• DescriptiveComplexity.Draw.dblPt b a = (b, fun (x : Fin 1) => a)

@[simp]

theorem DescriptiveComplexity.Draw.dblPt_fst {L : FirstOrder.Language} {A : Type} (b : Bool) (a : A) : (dblPt b a).1 = b

@[simp]

theorem DescriptiveComplexity.Draw.dblPt_snd {L : FirstOrder.Language} {A : Type} (b : Bool) (a : A) (j : Fin 1) : (dblPt b a).2 j = a

theorem DescriptiveComplexity.Draw.dblPt_eta {L : FirstOrder.Language} {A : Type} (p : (dblInterp L).Map A) : p = dblPt p.1 (p.2 0)

A point of the doubled universe is its tag and its single coordinate.

theorem DescriptiveComplexity.Draw.relMap_dbl_inl {L : FirstOrder.Language} [L.IsRelational] {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (r : L.Relations n) (xs : Fin n → (dblInterp L).Map A) : FirstOrder.Language.Structure.RelMap (newSym r) xs ↔ (∀ (i : Fin n), (xs i).1 = false) ∧ FirstOrder.Language.Structure.RelMap r fun (i : Fin n) => (xs i).2 0

A relation of the instance's vocabulary holds in the doubled universe exactly on the marked copy, of the elements it carries.

theorem DescriptiveComplexity.Draw.relMap_dbl_old {L : FirstOrder.Language} [L.IsRelational] {A : Type} [L.Structure A] [LinearOrder A] (xs : Fin 1 → (dblInterp L).Map A) : FirstOrder.Language.Structure.RelMap (oldNewSym L) xs ↔ (xs 0).1 = false

The mark holds exactly on the copy that carries the instance.

theorem DescriptiveComplexity.Draw.dblPt_ne {L : FirstOrder.Language} {A : Type} [Nonempty A] : dblPt false (Classical.arbitrary A) ≠ dblPt true (Classical.arbitrary A)

The doubled universe is never a singleton: that is the whole point.

An environment to name constants in

The rule-definability discharge (DescriptiveComplexity.Draw.Data.uRulesDefinable_progOf) asks for one DescriptiveComplexity.Draw.Env, and only to name the gate dispatch's default tag – a nonemptiness of a type the instance does not mention, so any environment will do. The two-element one below is the cheapest: the structure in which nothing holds.

noncomputable def DescriptiveComplexity.Draw.boolEnv (L : FirstOrder.Language) [L.IsRelational] : Env L

The two-element environment over a relational vocabulary: the structure in which nothing holds, with the two Booleans as its designated elements.

Equations

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