The expansion whose points are the relations on the instance

What EPR's membership is read over. DescriptiveComplexity.AddrExp.addrExp has a block of one unary variable, so its points are the subsets of the instance; here the block's variable is binary, so a point is a binary relation – and an assignment of the universal variables of an ∃*∀* sentence is exactly that, a function being a relation.

Three tags keep the smaller objects visible inside the expansion:

• elt, whose points are the singletons of the diagonal – one per element of the instance;
• pair, whose points are the singletons – one per ordered pair of elements, which is what lets every symbol of the expanded vocabulary stay binary: a ternary fact about the instance is read as a binary one about a pair;
• asg, whose points are unrestricted – the assignments themselves.

The size is what the class needs: with n elements there are 2^(n²) points, so a Σ₁ sentence read here is a nondeterministic computation of exponential time in a polynomial of the instance, which is what NEXPTIME is.

The block and the vocabularies

@[reducible]

def DescriptiveComplexity.Epr.pairBlock : SOBlock

The block of the expansion: one binary relation variable, so an assignment of it is a binary relation on the instance.

Marked @[reducible] so that the numerals of a tuple of its arity elaborate.

Equations

• DescriptiveComplexity.Epr.pairBlock = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => 2 }

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peOrd : FirstOrder.Language

The instance's vocabulary together with the order, over which the defining sentences of the expansion live.

Equations

• DescriptiveComplexity.Epr.peOrd = FirstOrder.Language.epr.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peLang1 : FirstOrder.Language

One copy of the block.

Equations

• DescriptiveComplexity.Epr.peLang1 = DescriptiveComplexity.Epr.peOrd.sum DescriptiveComplexity.Epr.pairBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peLang2 : FirstOrder.Language

Two copies of the block.

Equations

• DescriptiveComplexity.Epr.peLang2 = DescriptiveComplexity.Epr.peLang1.sum DescriptiveComplexity.Epr.pairBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peSym1 : peLang1.Relations 2

The block's variable, in the one-copy vocabulary.

Equations

• DescriptiveComplexity.Epr.peSym1 = Sum.inr ⟨(), DescriptiveComplexity.Epr.peSym1._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peSymA : peLang2.Relations 2

The first copy's variable, in the two-copy vocabulary.

Equations

• DescriptiveComplexity.Epr.peSymA = Sum.inl (Sum.inr ⟨(), DescriptiveComplexity.Epr.peSym1._proof_1⟩)

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peSymB : peLang2.Relations 2

The second copy's variable, in the two-copy vocabulary.

Equations

• DescriptiveComplexity.Epr.peSymB = Sum.inr ⟨(), DescriptiveComplexity.Epr.peSym1._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.peIn {n : ℕ} (r : FirstOrder.Language.epr.Relations n) : peOrd.Relations n

An instance symbol, in the ordered vocabulary.

Equations

• DescriptiveComplexity.Epr.peIn r = Sum.inl r

Relations, as assignments of the block

def DescriptiveComplexity.Epr.peRel {A : Type} (ρ : pairBlock.Assignment A) : A → A → Prop

The relation an assignment of the block is.

Equations

• DescriptiveComplexity.Epr.peRel ρ x y = ρ () ![x, y]

def DescriptiveComplexity.Epr.peAssign {A : Type} (R : A → A → Prop) : pairBlock.Assignment A

And the assignment a relation is.

Equations

• DescriptiveComplexity.Epr.peAssign R x✝ v = R (v 0) (v 1)

@[simp]

theorem DescriptiveComplexity.Epr.peRel_peAssign {A : Type} (R : A → A → Prop) : peRel (peAssign R) = R

theorem DescriptiveComplexity.Epr.peAssign_peRel {A : Type} (ρ : pairBlock.Assignment A) : peAssign (peRel ρ) = ρ

theorem DescriptiveComplexity.Epr.peRel_injective {A : Type} : Function.Injective peRel

The atoms of the block and the lifts

noncomputable def DescriptiveComplexity.Epr.peF1 {γ : Type} (x y : γ) : peLang1.Formula γ

The block's variable, as a formula over one copy.

Equations

• DescriptiveComplexity.Epr.peF1 x y = DescriptiveComplexity.Epr.peSym1.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Epr.peFA {γ : Type} (x y : γ) : peLang2.Formula γ

The first copy's variable, as a formula over two copies.

Equations

• DescriptiveComplexity.Epr.peFA x y = DescriptiveComplexity.Epr.peSymA.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Epr.peFB {γ : Type} (x y : γ) : peLang2.Formula γ

The second copy's variable, as a formula over two copies.

Equations

• DescriptiveComplexity.Epr.peFB x y = DescriptiveComplexity.Epr.peSymB.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Epr.peMarkG {γ : Type} (r : FirstOrder.Language.epr.Relations 1) (x : γ) : peOrd.Formula γ

A unary relation of the instance, as a formula.

Equations

• DescriptiveComplexity.Epr.peMarkG r x = (DescriptiveComplexity.Epr.peIn r).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Epr.peBinG {γ : Type} (r : FirstOrder.Language.epr.Relations 2) (x y : γ) : peOrd.Formula γ

A binary relation of the instance, as a formula.

Equations

• DescriptiveComplexity.Epr.peBinG r x y = (DescriptiveComplexity.Epr.peIn r).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Epr.peTerG {γ : Type} (r : FirstOrder.Language.epr.Relations 3) (x y z : γ) : peOrd.Formula γ

A ternary relation of the instance, as a formula.

Equations

• DescriptiveComplexity.Epr.peTerG r x y z = (DescriptiveComplexity.Epr.peIn r).formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.Epr.peEqG {γ : Type} (x y : γ) : peOrd.Formula γ

Equality of two variables, as a formula.

Equations

• DescriptiveComplexity.Epr.peEqG x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Epr.peLift1 {γ : Type} (φ : peOrd.Formula γ) : peLang1.Formula γ

Reading a sentence of the base vocabulary in the one-copy vocabulary.

Equations

• DescriptiveComplexity.Epr.peLift1 φ = FirstOrder.Language.LHom.sumInl.onFormula φ

noncomputable def DescriptiveComplexity.Epr.peLift2 {γ : Type} (φ : peOrd.Formula γ) : peLang2.Formula γ

And in the two-copy vocabulary.

Equations

• DescriptiveComplexity.Epr.peLift2 φ = FirstOrder.Language.LHom.sumInl.onFormula (FirstOrder.Language.LHom.sumInl.onFormula φ)

@[simp]

theorem DescriptiveComplexity.Epr.realize_peF1 {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (ρ : pairBlock.Assignment A) (x y : γ) : (peF1 x y).Realize v ↔ peRel ρ (v x) (v y)

@[simp]

theorem DescriptiveComplexity.Epr.realize_peFA {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (ρ σ : pairBlock.Assignment A) (x y : γ) : (peFA x y).Realize v ↔ peRel ρ (v x) (v y)

@[simp]

theorem DescriptiveComplexity.Epr.realize_peFB {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (ρ σ : pairBlock.Assignment A) (x y : γ) : (peFB x y).Realize v ↔ peRel σ (v x) (v y)

@[simp]

theorem DescriptiveComplexity.Epr.realize_peMarkG {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (r : FirstOrder.Language.epr.Relations 1) (x : γ) : (peMarkG r x).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x]

@[simp]

theorem DescriptiveComplexity.Epr.realize_peBinG {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (r : FirstOrder.Language.epr.Relations 2) (x y : γ) : (peBinG r x y).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Epr.realize_peTerG {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (r : FirstOrder.Language.epr.Relations 3) (x y z : γ) : (peTerG r x y z).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x, v y, v z]

@[simp]

theorem DescriptiveComplexity.Epr.realize_peEqG {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (x y : γ) : (peEqG x y).Realize v ↔ v x = v y

@[simp]

theorem DescriptiveComplexity.Epr.realize_peLift1 {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (ρ : pairBlock.Assignment A) (φ : peOrd.Formula γ) : (peLift1 φ).Realize v ↔ φ.Realize v

@[simp]

theorem DescriptiveComplexity.Epr.realize_peLift2 {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] {v : γ → A} (ρ σ : pairBlock.Assignment A) (φ : peOrd.Formula γ) : (peLift2 φ).Realize v ↔ φ.Realize v

The tags and their domains

inductive DescriptiveComplexity.Epr.ETag : Type

The tags of the expansion: the elements, the ordered pairs, and the assignments.

• elt : ETag

  The point is an element of the instance.

• pair : ETag

  The point is an ordered pair of elements.

• asg : ETag

  The point is an assignment – any binary relation.

@[instance_reducible]

instance DescriptiveComplexity.Epr.instDecidableEqETag : DecidableEq ETag

Equations

• DescriptiveComplexity.Epr.instDecidableEqETag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.Epr.instFintypeETag : Fintype ETag

Equations

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

def DescriptiveComplexity.Epr.PEDiag {A : Type} (R : A → A → Prop) : Prop

A relation that is the diagonal singleton of an element: the reading that makes an element of the instance a point of the expansion.

Equations

• DescriptiveComplexity.Epr.PEDiag R = ∃ (x : A), ∀ (y z : A), R y z ↔ y = x ∧ z = x

def DescriptiveComplexity.Epr.PEPairRel {A : Type} (R : A → A → Prop) : Prop

A relation that is a singleton: the reading that makes an ordered pair one.

Equations

• DescriptiveComplexity.Epr.PEPairRel R = ∃ (x : A) (y : A), ∀ (z w : A), R z w ↔ z = x ∧ w = y

theorem DescriptiveComplexity.Epr.peDiag_diag {A : Type} (x : A) : PEDiag fun (y z : A) => y = x ∧ z = x

theorem DescriptiveComplexity.Epr.pePairRel_pair {A : Type} (x y : A) : PEPairRel fun (z w : A) => z = x ∧ w = y

noncomputable def DescriptiveComplexity.Epr.diagS : peLang1.Sentence

The domain sentence of the elements: the relation is a diagonal singleton.

Equations

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

noncomputable def DescriptiveComplexity.Epr.pairS : peLang1.Sentence

The domain sentence of the pairs: the relation is a singleton.

Equations

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

noncomputable def DescriptiveComplexity.Epr.domT : ETag → peLang1.Sentence

The domain sentence of each tag.

Equations

• DescriptiveComplexity.Epr.domT DescriptiveComplexity.Epr.ETag.elt = DescriptiveComplexity.Epr.diagS
• DescriptiveComplexity.Epr.domT DescriptiveComplexity.Epr.ETag.pair = DescriptiveComplexity.Epr.pairS
• DescriptiveComplexity.Epr.domT DescriptiveComplexity.Epr.ETag.asg = ⊤

@[simp]

theorem DescriptiveComplexity.Epr.realize_diagS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : pairBlock.Assignment A) : A ⊨ diagS ↔ PEDiag (peRel ρ)

@[simp]

theorem DescriptiveComplexity.Epr.realize_pairS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : pairBlock.Assignment A) : A ⊨ pairS ↔ PEPairRel (peRel ρ)

inductive FirstOrder.Language.eprPtRel : ℕ → Type

Relation symbols of the vocabulary the expansion's points are read in: the three kinds of point, the instance's own relations read at elements, the components of a pair, the argument of a literal-position pair, and membership of a pair in an assignment. Every symbol is unary or binary, the pairs being points of their own.

• isElt : eprPtRel 1

  isElt p: the point p is an element of the instance.

• isPair : eprPtRel 1

  isPair p: the point p is an ordered pair of elements.

• isAsg : eprPtRel 1

  isAsg p: the point p is an assignment.

• evarE : eprPtRel 1

  evarE x: the element x is an existential variable.

• clE : eprPtRel 1

  clE c: the element c is a clause.

• inClE : eprPtRel 2

  inClE c l: the literal l occurs in the clause c.

• posLE : eprPtRel 2

  posLE l s: the literal l is the positive atom of s.

• negLE : eprPtRel 2

  negLE l s: the literal l is the negated atom of s.

• sigE : eprPtRel 2

  sigE s p: the symbol s has the argument position p.

• fstP : eprPtRel 2

  fstP q x: the first component of the pair q is x.

• sndP : eprPtRel 2

  sndP q y: the second component of the pair q is y.

• argP : eprPtRel 2

  argP q x: the pair q is a literal and a position whose argument is the variable x.

• memP : eprPtRel 2

  memP r q: the assignment r contains the pair q.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqEprPtRel {a✝ : ℕ} : DecidableEq (eprPtRel a✝)

Equations

• FirstOrder.Language.instDecidableEqEprPtRel = FirstOrder.Language.instDecidableEqEprPtRel.decEq

def FirstOrder.Language.instDecidableEqEprPtRel.decEq {a✝ : ℕ} (x✝ x✝¹ : eprPtRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.eprPt : Language

The vocabulary of the expansion's points.

Equations

• FirstOrder.Language.eprPt = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.eprPtRel }

instance FirstOrder.Language.instIsRelationalEprPt : Language.eprPt.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.peIsEltSym : Language.eprPt.Relations 1

The symbol marking the points that are elements.

Equations

• FirstOrder.Language.peIsEltSym = FirstOrder.Language.eprPtRel.isElt

@[reducible, inline]

abbrev FirstOrder.Language.peIsPairSym : Language.eprPt.Relations 1

The symbol marking the points that are pairs.

Equations

• FirstOrder.Language.peIsPairSym = FirstOrder.Language.eprPtRel.isPair

@[reducible, inline]

abbrev FirstOrder.Language.peIsAsgSym : Language.eprPt.Relations 1

The symbol marking the points that are assignments.

Equations

• FirstOrder.Language.peIsAsgSym = FirstOrder.Language.eprPtRel.isAsg

@[reducible, inline]

abbrev FirstOrder.Language.peEVarSym : Language.eprPt.Relations 1

The existential-variable symbol, at the points.

Equations

• FirstOrder.Language.peEVarSym = FirstOrder.Language.eprPtRel.evarE

@[reducible, inline]

abbrev FirstOrder.Language.peClSym : Language.eprPt.Relations 1

The clause symbol, at the points.

Equations

• FirstOrder.Language.peClSym = FirstOrder.Language.eprPtRel.clE

@[reducible, inline]

abbrev FirstOrder.Language.peInClSym : Language.eprPt.Relations 2

The literal-of-a-clause symbol, at the points.

Equations

• FirstOrder.Language.peInClSym = FirstOrder.Language.eprPtRel.inClE

@[reducible, inline]

abbrev FirstOrder.Language.pePosSym : Language.eprPt.Relations 2

The positive-literal symbol, at the points.

Equations

• FirstOrder.Language.pePosSym = FirstOrder.Language.eprPtRel.posLE

@[reducible, inline]

abbrev FirstOrder.Language.peNegSym : Language.eprPt.Relations 2

The negated-literal symbol, at the points.

Equations

• FirstOrder.Language.peNegSym = FirstOrder.Language.eprPtRel.negLE

@[reducible, inline]

abbrev FirstOrder.Language.peSigSym : Language.eprPt.Relations 2

The signature symbol, at the points.

Equations

• FirstOrder.Language.peSigSym = FirstOrder.Language.eprPtRel.sigE

@[reducible, inline]

abbrev FirstOrder.Language.peFstSym : Language.eprPt.Relations 2

The first-component symbol.

Equations

• FirstOrder.Language.peFstSym = FirstOrder.Language.eprPtRel.fstP

@[reducible, inline]

abbrev FirstOrder.Language.peSndSym : Language.eprPt.Relations 2

The second-component symbol.

Equations

• FirstOrder.Language.peSndSym = FirstOrder.Language.eprPtRel.sndP

@[reducible, inline]

abbrev FirstOrder.Language.peArgSym : Language.eprPt.Relations 2

The argument symbol, read at a literal-position pair.

Equations

• FirstOrder.Language.peArgSym = FirstOrder.Language.eprPtRel.argP

@[reducible, inline]

abbrev FirstOrder.Language.peMemSym : Language.eprPt.Relations 2

The membership symbol of an assignment.

Equations

• FirstOrder.Language.peMemSym = FirstOrder.Language.eprPtRel.memP

The defining sentences

noncomputable def DescriptiveComplexity.Epr.onS1 (φ : peLang1.Sentence) : (peOrd.sum (pairBlock.replicate 1).lang).Sentence

Reading a one-copy sentence inside the block replicated once.

Equations

• DescriptiveComplexity.Epr.onS1 φ = (DescriptiveComplexity.SOBlock.oneLHom DescriptiveComplexity.Epr.peOrd DescriptiveComplexity.Epr.pairBlock).onSentence φ

noncomputable def DescriptiveComplexity.Epr.onS2 (φ : peLang2.Sentence) : (peOrd.sum (pairBlock.replicate 2).lang).Sentence

Reading a two-copy sentence inside the block replicated twice.

Equations

• DescriptiveComplexity.Epr.onS2 φ = (DescriptiveComplexity.SOBlock.twoLHom DescriptiveComplexity.Epr.peOrd DescriptiveComplexity.Epr.pairBlock).onSentence φ

noncomputable def DescriptiveComplexity.Epr.tagS1 (b : Prop) : peLang1.Sentence

A static choice on the tags.

Equations

• DescriptiveComplexity.Epr.tagS1 b = if b then ⊤ else ⊥

noncomputable def DescriptiveComplexity.Epr.markS (r : FirstOrder.Language.epr.Relations 1) : peLang1.Sentence

A mark of the instance, at an element: the point is the element x, and x carries the mark.

Equations

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

noncomputable def DescriptiveComplexity.Epr.binS (r : FirstOrder.Language.epr.Relations 2) : peLang2.Sentence

A binary relation of the instance, at two elements.

Equations

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

noncomputable def DescriptiveComplexity.Epr.fstS : peLang2.Sentence

The first component of a pair: the pair is (x, y) and the second point is the element x.

Equations

• DescriptiveComplexity.Epr.fstS = FirstOrder.Language.Formula.iExs (Fin 2) (DescriptiveComplexity.Epr.peFA (Sum.inr 0) (Sum.inr 1) ⊓ DescriptiveComplexity.Epr.peFB (Sum.inr 0) (Sum.inr 0))

noncomputable def DescriptiveComplexity.Epr.sndS : peLang2.Sentence

The second component of a pair.

Equations

• DescriptiveComplexity.Epr.sndS = FirstOrder.Language.Formula.iExs (Fin 2) (DescriptiveComplexity.Epr.peFA (Sum.inr 0) (Sum.inr 1) ⊓ DescriptiveComplexity.Epr.peFB (Sum.inr 1) (Sum.inr 1))

noncomputable def DescriptiveComplexity.Epr.argS : peLang2.Sentence

The argument of a literal at a position: the pair is a literal l and a position p, the second point is the element x, and the encoding declares x there.

Equations

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

noncomputable def DescriptiveComplexity.Epr.memS : peLang2.Sentence

A pair belongs to an assignment: the second point is the pair (x, y) and the first, as a relation, holds of x and y.

Equations

• DescriptiveComplexity.Epr.memS = FirstOrder.Language.Formula.iExs (Fin 2) (DescriptiveComplexity.Epr.peFB (Sum.inr 0) (Sum.inr 1) ⊓ DescriptiveComplexity.Epr.peFA (Sum.inr 0) (Sum.inr 1))

noncomputable def DescriptiveComplexity.Epr.unT (r : FirstOrder.Language.epr.Relations 1) : ETag → peLang1.Sentence

The defining sentence of a unary symbol at a tag.

Equations

• DescriptiveComplexity.Epr.unT r DescriptiveComplexity.Epr.ETag.elt = DescriptiveComplexity.Epr.markS r
• DescriptiveComplexity.Epr.unT r x✝ = ⊥

noncomputable def DescriptiveComplexity.Epr.binT (r : FirstOrder.Language.epr.Relations 2) : ETag → ETag → peLang2.Sentence

The defining sentence of a binary symbol at a pair of tags: both points must be elements.

Equations

• DescriptiveComplexity.Epr.binT r DescriptiveComplexity.Epr.ETag.elt DescriptiveComplexity.Epr.ETag.elt = DescriptiveComplexity.Epr.binS r
• DescriptiveComplexity.Epr.binT r x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.Epr.compT (φ : peLang2.Sentence) : ETag → ETag → peLang2.Sentence

The defining sentence of the two component symbols.

Equations

• DescriptiveComplexity.Epr.compT φ DescriptiveComplexity.Epr.ETag.pair DescriptiveComplexity.Epr.ETag.elt = φ
• DescriptiveComplexity.Epr.compT φ x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.Epr.memT : ETag → ETag → peLang2.Sentence

The defining sentence of the membership symbol.

Equations

• DescriptiveComplexity.Epr.memT DescriptiveComplexity.Epr.ETag.asg DescriptiveComplexity.Epr.ETag.pair = DescriptiveComplexity.Epr.memS
• DescriptiveComplexity.Epr.memT x✝¹ x✝ = ⊥

noncomputable def DescriptiveComplexity.Epr.eprExp : ExpExpansion FirstOrder.Language.epr

The expansion whose points are the relations on the instance.

Equations

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

Reading the expansion at its points

@[instance_reducible]

noncomputable def DescriptiveComplexity.Epr.eprPtStructure (A : Type) [FirstOrder.Language.epr.Structure A] [LinearOrder A] : FirstOrder.Language.eprPt.Structure (eprExp.Map A)

The expanded structure, at the vocabulary of the points – equal to the expansion's own by definition, but not syntactically, so instance search has to be handed it.

Equations

• DescriptiveComplexity.Epr.eprPtStructure A = DescriptiveComplexity.Epr.eprExp.mapStructure A

theorem DescriptiveComplexity.Epr.realize_one {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (rt : FirstOrder.Language.eprPt.Relations 1) (φ : ETag → peLang1.Sentence) (h : ∀ (τ : Fin 1 → ETag), eprExp.relSentence rt τ = onS1 (φ (τ 0))) (x : eprExp.Map A) : FirstOrder.Language.Structure.RelMap rt ![x] ↔ A ⊨ φ (↑x).1

Reading a unary symbol of the expanded vocabulary at one point.

theorem DescriptiveComplexity.Epr.realize_two {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (rt : FirstOrder.Language.eprPt.Relations 2) (φ : ETag → ETag → peLang2.Sentence) (h : ∀ (τ : Fin 2 → ETag), eprExp.relSentence rt τ = onS2 (φ (τ 0) (τ 1))) (x y : eprExp.Map A) : FirstOrder.Language.Structure.RelMap rt ![x, y] ↔ A ⊨ φ (↑x).1 (↑y).1

Reading a binary symbol of the expanded vocabulary at two points.

The three kinds of point

theorem DescriptiveComplexity.Epr.domHolds_elt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x : A) : ExpExpansion.DomHolds (ETag.elt, peAssign fun (y z : A) => y = x ∧ z = x)

theorem DescriptiveComplexity.Epr.domHolds_pair {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y : A) : ExpExpansion.DomHolds (ETag.pair, peAssign fun (z w : A) => z = x ∧ w = y)

theorem DescriptiveComplexity.Epr.domHolds_asg {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) : ExpExpansion.DomHolds (ETag.asg, peAssign R)

noncomputable def DescriptiveComplexity.Epr.eltPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x : A) : eprExp.Map A

The point an element is: the diagonal singleton, tagged elt.

Equations

• DescriptiveComplexity.Epr.eltPt x = ⟨(DescriptiveComplexity.Epr.ETag.elt, DescriptiveComplexity.Epr.peAssign fun (y z : A) => y = x ∧ z = x), ⋯⟩

noncomputable def DescriptiveComplexity.Epr.pairPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y : A) : eprExp.Map A

The point an ordered pair is.

Equations

• DescriptiveComplexity.Epr.pairPt x y = ⟨(DescriptiveComplexity.Epr.ETag.pair, DescriptiveComplexity.Epr.peAssign fun (z w : A) => z = x ∧ w = y), ⋯⟩

noncomputable def DescriptiveComplexity.Epr.asgPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) : eprExp.Map A

The point an assignment is.

Equations

• DescriptiveComplexity.Epr.asgPt R = ⟨(DescriptiveComplexity.Epr.ETag.asg, DescriptiveComplexity.Epr.peAssign R), ⋯⟩

@[simp]

theorem DescriptiveComplexity.Epr.eltPt_tag {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x : A) : (↑(eltPt x)).1 = ETag.elt

@[simp]

theorem DescriptiveComplexity.Epr.pairPt_tag {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y : A) : (↑(pairPt x y)).1 = ETag.pair

@[simp]

theorem DescriptiveComplexity.Epr.asgPt_tag {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) : (↑(asgPt R)).1 = ETag.asg

theorem DescriptiveComplexity.Epr.eltPt_injective {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] : Function.Injective eltPt

theorem DescriptiveComplexity.Epr.cases_point {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : (∃ (x : A), p = eltPt x) ∨ (∃ (x : A) (y : A), p = pairPt x y) ∨ ∃ (R : A → A → Prop), p = asgPt R

Every point is an element, a pair or an assignment: what the domain sentences say, read back.

What the defining sentences say

@[simp]

theorem DescriptiveComplexity.Epr.realize_tagS1 {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (b : Prop) (ρ : pairBlock.Assignment A) : A ⊨ tagS1 b ↔ b

@[simp]

theorem DescriptiveComplexity.Epr.realize_markS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (r : FirstOrder.Language.epr.Relations 1) (ρ : pairBlock.Assignment A) : A ⊨ markS r ↔ ∃ (x : A), peRel ρ x x ∧ FirstOrder.Language.Structure.RelMap r ![x]

@[simp]

theorem DescriptiveComplexity.Epr.realize_binS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (r : FirstOrder.Language.epr.Relations 2) (ρ σ : pairBlock.Assignment A) : A ⊨ binS r ↔ ∃ (x : A) (y : A), peRel ρ x x ∧ peRel σ y y ∧ FirstOrder.Language.Structure.RelMap r ![x, y]

@[simp]

theorem DescriptiveComplexity.Epr.realize_fstS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ σ : pairBlock.Assignment A) : A ⊨ fstS ↔ ∃ (x : A) (y : A), peRel ρ x y ∧ peRel σ x x

@[simp]

theorem DescriptiveComplexity.Epr.realize_sndS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ σ : pairBlock.Assignment A) : A ⊨ sndS ↔ ∃ (x : A) (y : A), peRel ρ x y ∧ peRel σ y y

@[simp]

theorem DescriptiveComplexity.Epr.realize_argS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ σ : pairBlock.Assignment A) : A ⊨ argS ↔ ∃ (l : A) (p : A) (x : A), peRel ρ l p ∧ peRel σ x x ∧ ArgG l p x

@[simp]

theorem DescriptiveComplexity.Epr.realize_memS {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ σ : pairBlock.Assignment A) : A ⊨ memS ↔ ∃ (x : A) (y : A), peRel σ x y ∧ peRel ρ x y

What the symbols say at the points

@[simp]

theorem DescriptiveComplexity.Epr.peRel_eltPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y z : A) : peRel (↑(eltPt x)).2 y z ↔ y = x ∧ z = x

@[simp]

theorem DescriptiveComplexity.Epr.peRel_pairPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y z w : A) : peRel (↑(pairPt x y)).2 z w ↔ z = x ∧ w = y

@[simp]

theorem DescriptiveComplexity.Epr.peRel_asgPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) (x y : A) : peRel (↑(asgPt R)).2 x y ↔ R x y

theorem DescriptiveComplexity.Epr.realize_isElt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peIsEltSym ![p] ↔ (↑p).1 = ETag.elt

theorem DescriptiveComplexity.Epr.realize_isPair {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peIsPairSym ![p] ↔ (↑p).1 = ETag.pair

theorem DescriptiveComplexity.Epr.realize_isAsg {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peIsAsgSym ![p] ↔ (↑p).1 = ETag.asg

theorem DescriptiveComplexity.Epr.realize_un {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (rt : FirstOrder.Language.eprPt.Relations 1) (r : FirstOrder.Language.epr.Relations 1) (h : ∀ (τ : Fin 1 → ETag), eprExp.relSentence rt τ = onS1 (unT r (τ 0))) (x : A) : FirstOrder.Language.Structure.RelMap rt ![eltPt x] ↔ FirstOrder.Language.Structure.RelMap r ![x]

A unary mark of the instance, read at the point of an element.

theorem DescriptiveComplexity.Epr.realize_bin {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (rt : FirstOrder.Language.eprPt.Relations 2) (r : FirstOrder.Language.epr.Relations 2) (h : ∀ (τ : Fin 2 → ETag), eprExp.relSentence rt τ = onS2 (binT r (τ 0) (τ 1))) (x y : A) : FirstOrder.Language.Structure.RelMap rt ![eltPt x, eltPt y] ↔ FirstOrder.Language.Structure.RelMap r ![x, y]

A binary relation of the instance, read at the points of two elements.

theorem DescriptiveComplexity.Epr.realize_evarE {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peEVarSym ![eltPt x] ↔ EVarG x

theorem DescriptiveComplexity.Epr.realize_clE {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (c : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peClSym ![eltPt c] ↔ ClauseG c

theorem DescriptiveComplexity.Epr.realize_inClE {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (c l : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peInClSym ![eltPt c, eltPt l] ↔ InClG c l

theorem DescriptiveComplexity.Epr.realize_posLE {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l s : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.pePosSym ![eltPt l, eltPt s] ↔ PosG l s

theorem DescriptiveComplexity.Epr.realize_negLE {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l s : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peNegSym ![eltPt l, eltPt s] ↔ NegG l s

theorem DescriptiveComplexity.Epr.realize_sigE {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (s p : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peSigSym ![eltPt s, eltPt p] ↔ SigG s p

theorem DescriptiveComplexity.Epr.realize_fstP {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y z : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peFstSym ![pairPt x y, eltPt z] ↔ z = x

theorem DescriptiveComplexity.Epr.realize_sndP {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y z : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peSndSym ![pairPt x y, eltPt z] ↔ z = y

theorem DescriptiveComplexity.Epr.realize_argP {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l p x : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peArgSym ![pairPt l p, eltPt x] ↔ ArgG l p x

theorem DescriptiveComplexity.Epr.realize_memP {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) (x y : A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.peMemSym ![asgPt R, pairPt x y] ↔ R x y