Trading an expansion's domain for a mark

An expansion carves its universe out of the tagged assignments by a domain sentence, and that is what makes walking it hard over the base: the immediate successor of a point is the least point above it, and skipping the tagged assignments that fail the domain sentence is not a first-order condition – “no point in between” quantifies over block assignments.

This file removes the difficulty at the source. X.trivialize is the same expansion with the same tags and the same block, its domain sentence replaced by ⊤ and the old domain kept as a new unary symbol of the expanded vocabulary. Its universe is therefore every tagged assignment, where the successor is the plain binary increment (DescriptiveComplexity.SOBlock.succAssignF), and the old universe is the part the mark selects.

What has to move along is the problem: a walk over the old universe becomes a walk over the new one whose formulas are relativized to the mark (DescriptiveComplexity.ExpExpansion.relSpec), which is the standard guard insertion of DescriptiveComplexity.relativizeTo together with the renaming of the vocabulary. The two are done by one recursion here (DescriptiveComplexity.ExpExpansion.relLift) rather than composed, so that its correctness is a single induction stated directly at the inclusion of the old universe into the new – which is what the walk correspondence consumes.

The inclusion is definitional: the trivialized expansion has the same tags and the same block, so its points are the same pairs, its order is the same order, and its relations are given by the same sentences. Nothing but the domain condition changes, and that is a proof field of the subtype.

The marking vocabulary

inductive DescriptiveComplexity.markRel : ℕ → Type

Relation symbols of the marking vocabulary: one unary symbol.

• real : markRel 1

  real x: the point x was in the domain of the original expansion.

def DescriptiveComplexity.instDecidableEqMarkRel.decEq {a✝ : ℕ} (x✝ x✝¹ : markRel a✝) : Decidable (x✝ = x✝¹)

Equations

• DescriptiveComplexity.instDecidableEqMarkRel.decEq DescriptiveComplexity.markRel.real DescriptiveComplexity.markRel.real = isTrue DescriptiveComplexity.instDecidableEqMarkRel.decEq._proof_1

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqMarkRel {a✝ : ℕ} : DecidableEq (markRel a✝)

Equations

• DescriptiveComplexity.instDecidableEqMarkRel = DescriptiveComplexity.instDecidableEqMarkRel.decEq

def DescriptiveComplexity.markLang : FirstOrder.Language

The vocabulary of a single unary relation, marking the points an expansion's domain sentence admits.

Equations

• DescriptiveComplexity.markLang = { Functions := fun (x : ℕ) => Empty, Relations := DescriptiveComplexity.markRel }

instance DescriptiveComplexity.instIsRelationalMarkLang : markLang.IsRelational

The trivialized expansion

def DescriptiveComplexity.ExpExpansion.rep1LHom {L : FirstOrder.Language} (X : ExpExpansion L) : (L.sum FirstOrder.Language.order).sum X.B.lang →ᴸ (L.sum FirstOrder.Language.order).sum (X.B.replicate 1).lang

Reading a sentence over one copy of the block inside the one-fold replication, which is the shape a defining sentence of a unary symbol has.

Equations

• X.rep1LHom = (FirstOrder.Language.LHom.id (L.sum FirstOrder.Language.order)).sumMap (DescriptiveComplexity.SOBlock.homLHom (fun (i : X.B.ι) => (0, i)) ⋯)

theorem DescriptiveComplexity.ExpExpansion.realize_rep1LHom {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin 1 → X.B.Assignment A) (φ : ((L.sum FirstOrder.Language.order).sum X.B.lang).Sentence) : A ⊨ X.rep1LHom.onSentence φ ↔ A ⊨ φ

noncomputable def DescriptiveComplexity.ExpExpansion.trivialize {L : FirstOrder.Language} (X : ExpExpansion L) : ExpExpansion L

The expansion with a trivial domain: the same tags and the same block, so the same candidate points, but every one of them admitted, the old domain sentence surviving as the defining sentence of a new unary symbol.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.realSym {L : FirstOrder.Language} (X : ExpExpansion L) : X.trivialize.E.Relations 1

The marking symbol of the trivialized vocabulary.

Equations

• X.realSym = Sum.inr DescriptiveComplexity.markRel.real

theorem DescriptiveComplexity.ExpExpansion.trivialize_domHolds {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.trivialize.Point A) : DomHolds p

Every candidate point is a point of the trivialized expansion.

def DescriptiveComplexity.ExpExpansion.trivPt {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.Point A) : X.trivialize.Map A

A point of the trivialized expansion, from a candidate point.

Equations

• DescriptiveComplexity.ExpExpansion.trivPt p = ⟨p, ⋯⟩

def DescriptiveComplexity.ExpExpansion.trivIncl {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (p : X.Map A) : X.trivialize.Map A

The inclusion of the original universe into the trivialized one.

Equations

• DescriptiveComplexity.ExpExpansion.trivIncl p = DescriptiveComplexity.ExpExpansion.trivPt ↑p

theorem DescriptiveComplexity.ExpExpansion.trivIncl_injective {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] : Function.Injective trivIncl

theorem DescriptiveComplexity.ExpExpansion.relMap_realSym {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (q : X.trivialize.Map A) : FirstOrder.Language.Structure.RelMap X.realSym ![q] ↔ DomHolds ↑q

The mark holds exactly of the old points.

theorem DescriptiveComplexity.ExpExpansion.relMap_trivIncl {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {n : ℕ} (r : X.E.Relations n) (xs : Fin n → X.Map A) : (FirstOrder.Language.Structure.RelMap (Sum.inl r) fun (i : Fin n) => trivIncl (xs i)) ↔ FirstOrder.Language.Structure.RelMap r xs

The relations are unchanged: a relation of the original vocabulary holds of included points exactly when it held of them.

theorem DescriptiveComplexity.ExpExpansion.exists_trivIncl_iff {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (q : X.trivialize.Map A) : (∃ (p : X.Map A), trivIncl p = q) ↔ FirstOrder.Language.Structure.RelMap X.realSym ![q]

The included points are exactly the marked ones.

theorem DescriptiveComplexity.ExpExpansion.trivIncl_le_iff {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (p q : X.Map A) : trivIncl p ≤ trivIncl q ↔ p ≤ q

The order is unchanged: the trivialized expansion orders its points by the same key, tag first and then the assignment as a binary number.

Relativizing a formula to the mark

def DescriptiveComplexity.ExpExpansion.termLift {L : FirstOrder.Language} (X : ExpExpansion L) {β : Type} : (X.E.sum FirstOrder.Language.order).Term β → (X.trivialize.E.sum FirstOrder.Language.order).Term β

A term of the original vocabulary, read in the marked one: over relational vocabularies a term is a variable, so there is nothing to do.

Equations

• X.termLift (FirstOrder.Language.var x_1) = FirstOrder.Language.var x_1
• X.termLift (FirstOrder.Language.func f _ts) = isEmptyElim f

noncomputable def DescriptiveComplexity.ExpExpansion.symLift {L : FirstOrder.Language} (X : ExpExpansion L) {n : ℕ} : (X.E.sum FirstOrder.Language.order).Relations n → (X.trivialize.E.sum FirstOrder.Language.order).Relations n

A relation symbol of the original vocabulary, in the marked one.

Equations

• X.symLift (Sum.inl s) = Sum.inl (Sum.inl s)
• X.symLift (Sum.inr o) = Sum.inr o

noncomputable def DescriptiveComplexity.ExpExpansion.markGuard {L : FirstOrder.Language} (X : ExpExpansion L) {β : Type} (n : ℕ) : (X.trivialize.E.sum FirstOrder.Language.order).BoundedFormula β (n + 1)

The guard “the last bound variable is marked”.

Equations

• X.markGuard n = FirstOrder.Language.Relations.boundedFormula₁ (Sum.inl X.realSym) (FirstOrder.Language.var (Sum.inr (Fin.last n)))

noncomputable def DescriptiveComplexity.ExpExpansion.markF {L : FirstOrder.Language} (X : ExpExpansion L) {β : Type} (x : β) : (X.trivialize.E.sum FirstOrder.Language.order).Formula β

The mark, as a formula of one variable.

Equations

• X.markF x = FirstOrder.Language.Relations.boundedFormula₁ (Sum.inl X.realSym) (FirstOrder.Language.var (Sum.inl x))

noncomputable def DescriptiveComplexity.ExpExpansion.relLift {L : FirstOrder.Language} (X : ExpExpansion L) {β : Type} {n : ℕ} : (X.E.sum FirstOrder.Language.order).BoundedFormula β n → (X.trivialize.E.sum FirstOrder.Language.order).BoundedFormula β n

Lifting and relativizing at once: the formula read in the trivialized expansion, with every quantifier restricted to the marked points. Composing FirstOrder.Language.LHom.onBoundedFormula with DescriptiveComplexity.relativizeTo would do the same, but this way its correctness is one induction, stated directly at the inclusion of the old universe into the new.

Equations

• X.relLift FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
• X.relLift (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.BoundedFormula.equal (X.termLift t₁) (X.termLift t₂)
• X.relLift (FirstOrder.Language.BoundedFormula.rel r ts) = FirstOrder.Language.BoundedFormula.rel (X.symLift r) fun (i : Fin l) => X.termLift (ts i)
• X.relLift (φ.imp ψ) = (X.relLift φ).imp (X.relLift ψ)
• X.relLift φ.all = ((X.markGuard x✝).imp (X.relLift φ)).all

theorem DescriptiveComplexity.ExpExpansion.realize_termLift {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} (v : β → X.Map A) (t : (X.E.sum FirstOrder.Language.order).Term β) : FirstOrder.Language.Term.realize (fun (b : β) => trivIncl (v b)) (X.termLift t) = trivIncl (FirstOrder.Language.Term.realize v t)

theorem DescriptiveComplexity.ExpExpansion.realize_termLift_elim {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} {n : ℕ} (v : β → X.Map A) (xs : Fin n → X.Map A) (t : (X.E.sum FirstOrder.Language.order).Term (β ⊕ Fin n)) : FirstOrder.Language.Term.realize (Sum.elim (fun (b : β) => trivIncl (v b)) fun (i : Fin n) => trivIncl (xs i)) (X.termLift t) = trivIncl (FirstOrder.Language.Term.realize (Sum.elim v xs) t)

theorem DescriptiveComplexity.ExpExpansion.realize_markF {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} (v : β → X.trivialize.Map A) (x : β) : (X.markF x).Realize v ↔ ∃ (p : X.Map A), trivIncl p = v x

theorem DescriptiveComplexity.ExpExpansion.realize_relLift {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} {n : ℕ} (φ : (X.E.sum FirstOrder.Language.order).BoundedFormula β n) (v : β → X.Map A) (xs : Fin n → X.Map A) : ((X.relLift φ).Realize (fun (b : β) => trivIncl (v b)) fun (i : Fin n) => trivIncl (xs i)) ↔ φ.Realize v xs

The relativized formula says of the marked points what the original said of the old ones.

theorem DescriptiveComplexity.ExpExpansion.realize_relLift_formula {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {β : Type} (φ : (X.E.sum FirstOrder.Language.order).Formula β) (v : β → X.Map A) : (FirstOrder.Language.Formula.Realize (X.relLift φ) fun (b : β) => trivIncl (v b)) ↔ φ.Realize v

The relativized formula, at no bound variables.

The walk, carried over

noncomputable def DescriptiveComplexity.ExpExpansion.relSpec {L : FirstOrder.Language} (X : ExpExpansion L) (spec : TCSpec X.E) : TCSpec X.trivialize.E

The walk of a specification, carried to the trivialized expansion: every formula relativized to the mark, and the mark of the tuple required wherever the walk enters a node – at a source, and at the target of a step.

Equations

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

def DescriptiveComplexity.ExpExpansion.relNode {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {spec : TCSpec X.E} (a : spec.Node (X.Map A)) : (X.relSpec spec).Node (X.trivialize.Map A)

A node of the carried walk: the same mode, the tuple included.

Equations

• DescriptiveComplexity.ExpExpansion.relNode a = (a.1, fun (i : Fin (X.relSpec spec).k) => DescriptiveComplexity.ExpExpansion.trivIncl (a.2 i))

theorem DescriptiveComplexity.ExpExpansion.realize_marks {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} {β : Type} (sel : Fin spec.k → β) (v : β → X.trivialize.Map A) : (listInf (List.map (fun (i : Fin spec.k) => X.markF (sel i)) (List.finRange spec.k))).Realize v ↔ ∀ (i : Fin spec.k), ∃ (p : X.Map A), trivIncl p = v (sel i)

The conjoined marks hold exactly of a tuple of included points.

theorem DescriptiveComplexity.ExpExpansion.isSrc_relNode {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} (a : spec.Node (X.Map A)) : (X.relSpec spec).IsSrc (relNode a) ↔ spec.IsSrc a

theorem DescriptiveComplexity.ExpExpansion.isTgt_relNode {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} (a : spec.Node (X.Map A)) : (X.relSpec spec).IsTgt (relNode a) ↔ spec.IsTgt a

theorem DescriptiveComplexity.ExpExpansion.step_relNode {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} (a b : spec.Node (X.Map A)) : (X.relSpec spec).Step (relNode a) (relNode b) ↔ spec.Step a b

theorem DescriptiveComplexity.ExpExpansion.exists_relNode {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {spec : TCSpec X.E} {u : (X.relSpec spec).Node (X.trivialize.Map A)} (h : ∀ (i : Fin (X.relSpec spec).k), ∃ (p : X.Map A), trivIncl p = u.2 i) : ∃ (a : spec.Node (X.Map A)), relNode a = u

A node whose points are all marked is the image of a node of the original walk.

theorem DescriptiveComplexity.ExpExpansion.exists_relNode_of_isSrc {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} {u : (X.relSpec spec).Node (X.trivialize.Map A)} (h : (X.relSpec spec).IsSrc u) : ∃ (a : spec.Node (X.Map A)), relNode a = u

theorem DescriptiveComplexity.ExpExpansion.exists_relNode_of_step {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} {u v : (X.relSpec spec).Node (X.trivialize.Map A)} (h : (X.relSpec spec).Step u v) : ∃ (b : spec.Node (X.Map A)), relNode b = v

theorem DescriptiveComplexity.ExpExpansion.reach_relSpec {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} (a : spec.Node (X.Map A)) {v : (X.relSpec spec).Node (X.trivialize.Map A)} : (X.relSpec spec).Reach (relNode a) v → ∃ (b : spec.Node (X.Map A)), relNode b = v ∧ spec.Reach a b

Reachability is carried over, in both directions: a walk of the carried specification that starts at an included node stays included, step by step.

theorem DescriptiveComplexity.ExpExpansion.reach_relNode {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} {a b : spec.Node (X.Map A)} : spec.Reach a b → (X.relSpec spec).Reach (relNode a) (relNode b)

theorem DescriptiveComplexity.ExpExpansion.accepts_relSpec {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {spec : TCSpec X.E} : (X.relSpec spec).Accepts (X.trivialize.Map A) ↔ spec.Accepts (X.Map A)

The carried walk accepts exactly what the original one did.