EPR is in NEXPTIME

The membership half. Read over the expansion whose points are the relations on the instance (DescriptiveComplexity.Epr.eprExp), the whole of EPR is one Σ₁ sentence:

guess a relation I between the symbols and the assignments; check that it is local, that the instance is well-formed, and that some assignment of the existential variables makes every clause true at every assignment of the universal variables.

Both quantifiers over assignments are first-order there, an assignment being a point, so the sentence has one second-order block and NEXPTIME is NP.exp.

The two layers

The kernel is written once as formulas over an arbitrary index of free variables, and read back in two steps: a semantic reading at arbitrary points (DescriptiveComplexity.Epr.MemPt and its siblings), and then a computation of those predicates at the three kinds of point, which is where DescriptiveComplexity.Epr.realize_memP and the rest of the expansion's API is used. Splitting the two keeps the formula layer free of case analysis.

The guess and its vocabulary

@[reducible]

def DescriptiveComplexity.Epr.ivBlock : SOBlock

The block the Σ₁ definition guesses: one binary relation variable, read as “the symbol s holds of the assignment w”.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.eprSOLang : FirstOrder.Language

The vocabulary of the kernel: the points, together with the guess.

Equations

• DescriptiveComplexity.Epr.eprSOLang = FirstOrder.Language.eprPt.sum DescriptiveComplexity.Epr.ivBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.ptS₁ (r : FirstOrder.Language.eprPt.Relations 1) : eprSOLang.Relations 1

A unary symbol of the points, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.Epr.ptS₁ r = Sum.inl r

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.ptS₂ (r : FirstOrder.Language.eprPt.Relations 2) : eprSOLang.Relations 2

A binary symbol of the points, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.Epr.ptS₂ r = Sum.inl r

@[reducible, inline]

abbrev DescriptiveComplexity.Epr.ivS : eprSOLang.Relations 2

The guessed symbol.

Equations

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

The atoms

noncomputable def DescriptiveComplexity.Epr.ptF₁ {γ : Type} (r : FirstOrder.Language.eprPt.Relations 1) (x : γ) : eprSOLang.Formula γ

A unary symbol of the points, as a formula.

Equations

• DescriptiveComplexity.Epr.ptF₁ r x = (DescriptiveComplexity.Epr.ptS₁ r).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Epr.ptF₂ {γ : Type} (r : FirstOrder.Language.eprPt.Relations 2) (x y : γ) : eprSOLang.Formula γ

A binary symbol of the points, as a formula.

Equations

• DescriptiveComplexity.Epr.ptF₂ r x y = (DescriptiveComplexity.Epr.ptS₂ r).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.Epr.ivF {γ : Type} (s w : γ) : eprSOLang.Formula γ

The guessed symbol, as a formula.

Equations

• DescriptiveComplexity.Epr.ivF s w = DescriptiveComplexity.Epr.ivS.formula₂ (FirstOrder.Language.var s) (FirstOrder.Language.var w)

noncomputable def DescriptiveComplexity.Epr.ptEqF {γ : Type} (x y : γ) : eprSOLang.Formula γ

Equality of two points.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.Epr.eprSOStructure {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) : eprSOLang.Structure (eprExp.Map A)

The structure the kernel is read in: the points, with the guess.

Equations

• DescriptiveComplexity.Epr.eprSOStructure ρ = FirstOrder.Language.eprPt.sumStructure DescriptiveComplexity.Epr.ivBlock.lang (DescriptiveComplexity.Epr.eprExp.Map A)

@[simp]

theorem DescriptiveComplexity.Epr.realize_ptF₁ {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (r : FirstOrder.Language.eprPt.Relations 1) (x : γ) : (ptF₁ r x).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x]

@[simp]

theorem DescriptiveComplexity.Epr.realize_ptF₂ {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (r : FirstOrder.Language.eprPt.Relations 2) (x y : γ) : (ptF₂ r x y).Realize v ↔ FirstOrder.Language.Structure.RelMap r ![v x, v y]

@[simp]

theorem DescriptiveComplexity.Epr.realize_ivF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (s w : γ) : (ivF s w).Realize v ↔ ρ () ![v s, v w]

@[simp]

theorem DescriptiveComplexity.Epr.realize_ptEqF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (x y : γ) : (ptEqF x y).Realize v ↔ v x = v y

The semantic reading, at arbitrary points

def DescriptiveComplexity.Epr.IsEltPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : Prop

The point is an element of the instance.

Equations

• DescriptiveComplexity.Epr.IsEltPt p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peIsEltSym ![p]

def DescriptiveComplexity.Epr.IsPairPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : Prop

The point is an ordered pair.

Equations

• DescriptiveComplexity.Epr.IsPairPt p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peIsPairSym ![p]

def DescriptiveComplexity.Epr.IsAsgPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (p : eprExp.Map A) : Prop

The point is an assignment.

Equations

• DescriptiveComplexity.Epr.IsAsgPt p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peIsAsgSym ![p]

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

The point q is the pair of x and y.

Equations

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

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

The assignment w sends x to y.

Equations

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

def DescriptiveComplexity.Epr.ArgPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l p x : eprExp.Map A) : Prop

The literal l names the variable x at the position p.

Equations

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

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

The element is an existential variable.

Equations

• DescriptiveComplexity.Epr.EVarPt x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peEVarSym ![x]

def DescriptiveComplexity.Epr.ClPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (c : eprExp.Map A) : Prop

The element is a clause.

Equations

• DescriptiveComplexity.Epr.ClPt c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peClSym ![c]

def DescriptiveComplexity.Epr.InClPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (c l : eprExp.Map A) : Prop

The literal occurs in the clause.

Equations

• DescriptiveComplexity.Epr.InClPt c l = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peInClSym ![c, l]

def DescriptiveComplexity.Epr.PosPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l s : eprExp.Map A) : Prop

The literal is the positive atom of the symbol.

Equations

• DescriptiveComplexity.Epr.PosPt l s = FirstOrder.Language.Structure.RelMap FirstOrder.Language.pePosSym ![l, s]

def DescriptiveComplexity.Epr.NegPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l s : eprExp.Map A) : Prop

The literal is the negated atom of the symbol.

Equations

• DescriptiveComplexity.Epr.NegPt l s = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peNegSym ![l, s]

def DescriptiveComplexity.Epr.SigPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (s p : eprExp.Map A) : Prop

The symbol has the argument position.

Equations

• DescriptiveComplexity.Epr.SigPt s p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.peSigSym ![s, p]

def DescriptiveComplexity.Epr.MatchPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l vv w : eprExp.Map A) : Prop

The assignment w of the argument positions matches the environment on the arguments the literal declares.

Equations

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

def DescriptiveComplexity.Epr.CombPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (e u w : eprExp.Map A) : Prop

The environment w is the one two assignments make.

Equations

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

def DescriptiveComplexity.Epr.TotalPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (w : eprExp.Map A) : Prop

Every element is sent somewhere by the assignment.

Equations

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

def DescriptiveComplexity.Epr.FuncPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (w : eprExp.Map A) : Prop

And to one place only.

Equations

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

def DescriptiveComplexity.Epr.LitTruePt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) (l vv : eprExp.Map A) : Prop

The literal l is true at the environment vv, under the guess ρ.

Equations

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

def DescriptiveComplexity.Epr.LocalPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) : Prop

The guess is local: the value of a symbol is decided by the arguments its signature declares.

Equations

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

def DescriptiveComplexity.Epr.WFPt (A : Type) [FirstOrder.Language.epr.Structure A] [LinearOrder A] : Prop

The instance is well-formed, read at the points.

Equations

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

@[simp]

theorem DescriptiveComplexity.Epr.isEltPt_eltPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x : A) : IsEltPt (eltPt x)

@[simp]

theorem DescriptiveComplexity.Epr.isPairPt_pairPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y : A) : IsPairPt (pairPt x y)

@[simp]

theorem DescriptiveComplexity.Epr.isAsgPt_asgPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) : IsAsgPt (asgPt R)

@[simp]

theorem DescriptiveComplexity.Epr.pairOfPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x y a b : A) : PairOfPt (pairPt x y) (eltPt a) (eltPt b) ↔ a = x ∧ b = y

@[simp]

theorem DescriptiveComplexity.Epr.memPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (R : A → A → Prop) (x y : A) : MemPt (asgPt R) (eltPt x) (eltPt y) ↔ R x y

@[simp]

theorem DescriptiveComplexity.Epr.eVarPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (x : A) : EVarPt (eltPt x) ↔ EVarG x

@[simp]

theorem DescriptiveComplexity.Epr.clPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (c : A) : ClPt (eltPt c) ↔ ClauseG c

@[simp]

theorem DescriptiveComplexity.Epr.inClPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (c l : A) : InClPt (eltPt c) (eltPt l) ↔ InClG c l

@[simp]

theorem DescriptiveComplexity.Epr.posPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l s : A) : PosPt (eltPt l) (eltPt s) ↔ PosG l s

@[simp]

theorem DescriptiveComplexity.Epr.negPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l s : A) : NegPt (eltPt l) (eltPt s) ↔ NegG l s

@[simp]

theorem DescriptiveComplexity.Epr.sigPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (s p : A) : SigPt (eltPt s) (eltPt p) ↔ SigG s p

@[simp]

theorem DescriptiveComplexity.Epr.argPt_iff {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (l p x : A) : ArgPt (eltPt l) (eltPt p) (eltPt x) ↔ ArgG l p x

The formulas of the kernel

noncomputable def DescriptiveComplexity.Epr.pairOfF {γ : Type} (q x y : γ) : eprSOLang.Formula γ

q is the pair of x and y.

Equations

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

noncomputable def DescriptiveComplexity.Epr.memF {γ : Type} (w x y : γ) : eprSOLang.Formula γ

The assignment w sends x to y.

Equations

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

noncomputable def DescriptiveComplexity.Epr.argF {γ : Type} (l p x : γ) : eprSOLang.Formula γ

The literal l names the variable x at the position p.

Equations

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

noncomputable def DescriptiveComplexity.Epr.totalF {γ : Type} (w : γ) : eprSOLang.Formula γ

Every element is sent somewhere by w.

Equations

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

noncomputable def DescriptiveComplexity.Epr.funcF {γ : Type} (w : γ) : eprSOLang.Formula γ

And to one place only.

Equations

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

@[simp]

theorem DescriptiveComplexity.Epr.realize_pairOfF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (q x y : γ) : (pairOfF q x y).Realize v ↔ PairOfPt (v q) (v x) (v y)

@[simp]

theorem DescriptiveComplexity.Epr.realize_memF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (w x y : γ) : (memF w x y).Realize v ↔ MemPt (v w) (v x) (v y)

@[simp]

theorem DescriptiveComplexity.Epr.realize_argF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (l p x : γ) : (argF l p x).Realize v ↔ ArgPt (v l) (v p) (v x)

@[simp]

theorem DescriptiveComplexity.Epr.realize_totalF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (w : γ) : (totalF w).Realize v ↔ TotalPt (v w)

@[simp]

theorem DescriptiveComplexity.Epr.realize_funcF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (w : γ) : (funcF w).Realize v ↔ FuncPt (v w)

The clauses of the kernel

noncomputable def DescriptiveComplexity.Epr.combF {γ : Type} (e u w : γ) : eprSOLang.Formula γ

The environment w is the one the two assignments make: the witness at an existential variable, the assignment being tested elsewhere.

Equations

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

noncomputable def DescriptiveComplexity.Epr.matchF {γ : Type} (l v w : γ) : eprSOLang.Formula γ

The assignment w of the argument positions matches the environment v on the arguments the literal l declares.

Equations

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

noncomputable def DescriptiveComplexity.Epr.litTrueF {γ : Type} (l v : γ) : eprSOLang.Formula γ

The literal l is true at the environment v.

Equations

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

noncomputable def DescriptiveComplexity.Epr.matrixF {γ : Type} (e : γ) : eprSOLang.Formula γ

Every clause is true at every assignment of the universal variables.

Equations

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

@[simp]

theorem DescriptiveComplexity.Epr.realize_combF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (e u w : γ) : (combF e u w).Realize v ↔ CombPt (v e) (v u) (v w)

@[simp]

theorem DescriptiveComplexity.Epr.realize_matchF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (l vv w : γ) : (matchF l vv w).Realize v ↔ MatchPt (v l) (v vv) (v w)

@[simp]

theorem DescriptiveComplexity.Epr.realize_litTrueF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (l vv : γ) : (litTrueF l vv).Realize v ↔ LitTruePt ρ (v l) (v vv)

@[simp]

theorem DescriptiveComplexity.Epr.realize_matrixF {γ A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) {v : γ → eprExp.Map A} (e : γ) : (matrixF e).Realize v ↔ ∀ (u w : eprExp.Map A), IsAsgPt u → TotalPt u → FuncPt u → IsAsgPt w → CombPt (v e) u w → ∀ (c : eprExp.Map A), IsEltPt c → ClPt c → ∃ (l : eprExp.Map A), IsEltPt l ∧ InClPt c l ∧ LitTruePt ρ l w

The kernel

noncomputable def DescriptiveComplexity.Epr.localF : eprSOLang.Sentence

The guess is local.

Equations

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

noncomputable def DescriptiveComplexity.Epr.wfF : eprSOLang.Sentence

The instance is well-formed: an atom names one variable at each position of its symbol's signature, and names one at each.

Equations

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

noncomputable def DescriptiveComplexity.Epr.eprKernel : eprSOLang.Sentence

The kernel of the Σ₁ definition: the instance is well-formed, the guess is local, and some assignment of the existential variables satisfies every clause at every assignment of the universal ones.

Equations

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

@[simp]

theorem DescriptiveComplexity.Epr.realize_localF {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) : eprExp.Map A ⊨ localF ↔ LocalPt ρ

@[simp]

theorem DescriptiveComplexity.Epr.realize_wfF {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) : eprExp.Map A ⊨ wfF ↔ WFPt A

@[simp]

theorem DescriptiveComplexity.Epr.realize_eprKernel {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (ρ : ivBlock.Assignment (eprExp.Map A)) : eprExp.Map A ⊨ eprKernel ↔ WFPt A ∧ LocalPt ρ ∧ ∃ (e : eprExp.Map A), (IsAsgPt e ∧ TotalPt e ∧ FuncPt e) ∧ ∀ (u w : eprExp.Map A), IsAsgPt u → TotalPt u → FuncPt u → IsAsgPt w → CombPt e u w → ∀ (c : eprExp.Map A), IsEltPt c → ClPt c → ∃ (l : eprExp.Map A), IsEltPt l ∧ InClPt c l ∧ LitTruePt ρ l w

The points a model is made of

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

The point a function is: its graph.

Equations

• DescriptiveComplexity.Epr.funPt f = DescriptiveComplexity.Epr.asgPt fun (a b : A) => f a = b

@[simp]

theorem DescriptiveComplexity.Epr.isAsgPt_funPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (f : A → A) : IsAsgPt (funPt f)

@[simp]

theorem DescriptiveComplexity.Epr.memPt_funPt {A : Type} [FirstOrder.Language.epr.Structure A] [LinearOrder A] (f : A → A) (x y : A) : MemPt (funPt f) (eltPt x) (eltPt y) ↔ f x = y

The agreement

The membership

theorem DescriptiveComplexity.Epr.epr_mem_NEXPTIME : NEXPTIME.Mem EPR

EPR is in NEXPTIME. The expansion's points are the relations on the instance, so an assignment of the universal variables is one of them and the ∀ that makes the problem exponential is first-order there; what is guessed is one relation between the symbols and the assignments, which is one Σ₁ block.