The block a problem over an expansion is guessed in

NEXPTIME ⊆ ∃SO[new, exp c d] rewrites a Σ₁ definition over an exponential expansion as a Σ₁ definition with value invention. Everything the rewritten sentence guesses goes into one second-order block, and this file is where that block is fixed and its symbols named:

• the order on the original elements, which the expansion's sentences need and the extended universe has none of – so the block is a DescriptiveComplexity.SOBlock.withOrder and DescriptiveComplexity.extLinearGuard is its guard;
• the meanings, one per variable of the expansion's block and one per tag – a tag is a nullary variable, so its meaning relation is unary, “this value carries this tag”;
• the source problem's own Σ₁ block, whose variables range over the points of the expansion and are therefore guessed over the extended universe and read at the values that are points.

What the file proves is that an assignment of that block reads as the data the translations of DescriptiveComplexity.SecondOrderNewRead and DescriptiveComplexity.SecondOrderNewPoint ask for (DescriptiveComplexity.pullPointOn), given only that its order part is a linear order of the original elements.

The block

@[reducible, inline]

abbrev DescriptiveComplexity.taggedBlock {L : FirstOrder.Language} (X : ExpExpansion L) : SOBlock

The expansion's block with one nullary variable per tag: what an invented value has to stand for is an assignment of this, the tag included.

Equations

• DescriptiveComplexity.taggedBlock X = X.B.cons (DescriptiveComplexity.tagBits X.Tag)

@[reducible, inline]

abbrev DescriptiveComplexity.guessBlock {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : SOBlock

Everything the sentence guesses besides the order: the meanings of the tagged block, and the source problem's own block.

Equations

• DescriptiveComplexity.guessBlock X C = (DescriptiveComplexity.meanBlockB (DescriptiveComplexity.taggedBlock X)).cons C

@[reducible, inline]

abbrev DescriptiveComplexity.pullBlock {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : SOBlock

The block: the order variable, the meanings, and the source problem's block.

Equations

• DescriptiveComplexity.pullBlock X C = (DescriptiveComplexity.guessBlock X C).withOrder

@[reducible, inline]

abbrev DescriptiveComplexity.pullLang {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : FirstOrder.Language

The vocabulary the guessed sentence is written in.

Equations

• DescriptiveComplexity.pullLang X C = (DescriptiveComplexity.newLang L).sum (DescriptiveComplexity.pullBlock X C).lang

The symbols

def DescriptiveComplexity.pullMeanSym {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) (i : X.B.ι) : (pullLang X C).Relations (X.B.arity i + 1)

The meaning relation of a variable of the expansion's block.

Equations

• DescriptiveComplexity.pullMeanSym X C i = Sum.inr ⟨Sum.inr (Sum.inl (Sum.inl i)), ⋯⟩

def DescriptiveComplexity.pullTagSym {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) (t : X.Tag) : (pullLang X C).Relations 1

The meaning relation of a tag: unary, the tag being a nullary variable.

Equations

• DescriptiveComplexity.pullTagSym X C t = Sum.inr ⟨Sum.inr (Sum.inl (Sum.inr t)), ⋯⟩

def DescriptiveComplexity.pullCertSym {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) (j : C.ι) : (pullLang X C).Relations (C.arity j)

A variable of the source problem's own block.

Equations

• DescriptiveComplexity.pullCertSym X C j = Sum.inr ⟨Sum.inr (Sum.inr j), ⋯⟩

def DescriptiveComplexity.pullReadSyms {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : ReadSyms L X.B (pullLang X C)

The symbols the translations of a defining sentence use.

Equations

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

def DescriptiveComplexity.pullPointSyms {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : PointSyms L X (pullLang X C)

The symbols the point formulas use.

Equations

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

What an assignment of the block reads as

def DescriptiveComplexity.pullMeans {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (v : A ⊕ Fin m) : X.B.Assignment A

The assignment of the expansion's block that an invented value means.

Equations

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

def DescriptiveComplexity.pullTags {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (v : A ⊕ Fin m) (t : X.Tag) : Prop

The tags an invented value carries.

Equations

• DescriptiveComplexity.pullTags ρ v t = ρ (Sum.inr (Sum.inl (Sum.inr t))) fun (x : Fin ((DescriptiveComplexity.pullBlock X C).arity (Sum.inr (Sum.inl (Sum.inr t))))) => v

def DescriptiveComplexity.pullLe {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (a b : A) : Prop

The order the order variable carries, as a relation on the instance.

Equations

• DescriptiveComplexity.pullLe ρ a b = ρ (Sum.inl ()) ![Sum.inl a, Sum.inl b]

@[instance_reducible]

noncomputable def DescriptiveComplexity.pullLinearOrder {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (hrefl : ∀ (a : A), pullLe ρ a a) (htrans : ∀ (a b c : A), pullLe ρ a b → pullLe ρ b c → pullLe ρ a c) (hanti : ∀ (a b : A), pullLe ρ a b → pullLe ρ b a → a = b) (htotal : ∀ (a b : A), pullLe ρ a b ∨ pullLe ρ b a) : LinearOrder A

The linear order the guard's order variable carries.

Equations

• DescriptiveComplexity.pullLinearOrder ρ hrefl htrans hanti htotal = DescriptiveComplexity.linearOrderOfGuard (fun (w : Fin 2 → A) => DescriptiveComplexity.pullLe ρ (w 0) (w 1)) hrefl ⋯ ⋯ ⋯

theorem DescriptiveComplexity.pullPointOn {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) [LinearOrder A] (hle : ∀ (a b : A), a ≤ b ↔ pullLe ρ a b) : PointOn (pullPointSyms X C) Sum.inl (pullMeans ρ) (pullTags ρ)

An assignment of the block reads as the data the translations ask for: its meaning variables give each invented value an assignment of the expansion's block, its tag variables the tags it carries, and its order variable the order of the instance – the last being a hypothesis, since which linear order the instance carries is the caller's to fix.

The kernel

noncomputable def DescriptiveComplexity.pullSubst {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (C : SOBlock) : FormulaSubst (X.E.sum C.lang) (pullLang X C)

The formulas interpreting the source problem's vocabulary – the expanded one together with its own block – over the extended universe: an atom of the expansion is DescriptiveComplexity.pointRelF, an atom of the block is the block variable itself.

Equations

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

noncomputable def DescriptiveComplexity.pullDom {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (C : SOBlock) : (pullLang X C).Formula (Fin 1)

The domain formula: the value is a point of the expanded universe.

Equations

• DescriptiveComplexity.pullDom X C = DescriptiveComplexity.isPointF (DescriptiveComplexity.pullPointSyms X C) 0

def DescriptiveComplexity.pullCert {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (e : X.Map A → A ⊕ Fin m) : C.Assignment (X.Map A)

The assignment of the source problem's block that the guess carries, read at the points.

Equations

• DescriptiveComplexity.pullCert ρ e j ts = ρ (Sum.inr (Sum.inr j)) fun (l : Fin ((DescriptiveComplexity.pullBlock X C).arity (Sum.inr (Sum.inr j)))) => e (ts l)

structure DescriptiveComplexity.PointRep {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (e : X.Map A → A ⊕ Fin m) : Prop

What names the points: an injection of the expanded universe into the invented values, whose image is exactly the values that are points, sending a point to a value that means its assignment and carries its tag and no other.

• inj : Function.Injective e

  Distinct points are named by distinct values.

• mean (p : X.Map A) : pullMeans ρ (e p) = (↑p).2

  A point's value means its assignment.

• tag (p : X.Map A) (t : X.Tag) : pullTags ρ (e p) t ↔ t = (↑p).1

  A point's value carries its tag and no other.

• onto (v : A ⊕ Fin m) : (∃ (t : X.Tag), pullTags ρ v t ∧ (∀ (t' : X.Tag), pullTags ρ v t' → t' = t) ∧ ExpExpansion.DomHolds (t, pullMeans ρ v)) → ∃ (p : X.Map A), e p = v

  Every value that is a point is named.

theorem DescriptiveComplexity.pullSubst_rel {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (h : PointOn (pullPointSyms X C) Sum.inl (pullMeans ρ) (pullTags ρ)) {e : X.Map A → A ⊕ Fin m} (hr : PointRep ρ e) {n : ℕ} (r : (X.E.sum C.lang).Relations n) (ts : Fin n → X.Map A) : FirstOrder.Language.Structure.RelMap r ts ↔ FirstOrder.Language.Structure.RelMap r ts

The structure the kernel's formulas define on the points is the one the source problem is read in: the expansion's own structure, and the source problem's block read at the values naming the points.

noncomputable def DescriptiveComplexity.pullSubstEquiv {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (h : PointOn (pullPointSyms X C) Sum.inl (pullMeans ρ) (pullTags ρ)) {e : X.Map A → A ⊕ Fin m} (hr : PointRep ρ e) : (X.E.sum C.lang).Equiv (X.Map A) (X.Map A)

The structure identification of DescriptiveComplexity.pullSubst_rel, as an isomorphism.

Equations

• DescriptiveComplexity.pullSubstEquiv ρ h hr = { toEquiv := Equiv.refl (X.Map A), map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.realize_pullKernel {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (h : PointOn (pullPointSyms X C) Sum.inl (pullMeans ρ) (pullTags ρ)) {e : X.Map A → A ⊕ Fin m} (hr : PointRep ρ e) (φ : (X.E.sum C.lang).Sentence) : (A ⊕ Fin m) ⊨ (pullSubst X C).substSentence (pullDom X C) φ ↔ X.Map A ⊨ φ

The kernel, translated: the source problem's first-order kernel, with DescriptiveComplexity.pointRelF for the atoms of the expanded vocabulary, its own block variables for its own, and “is a point” as the domain formula, holds in the extended universe exactly when the kernel holds over the expansion.

Naming the points

def DescriptiveComplexity.meanHom {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : (meanBlockB (taggedBlock X)).ι → (pullBlock X C).ι

The meaning block sits inside the whole block.

Equations

• DescriptiveComplexity.meanHom X C i = Sum.inr (Sum.inl i)

theorem DescriptiveComplexity.meanHom_arity {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) (i : (meanBlockB (taggedBlock X)).ι) : (pullBlock X C).arity (meanHom X C i) = (meanBlockB (taggedBlock X)).arity i

noncomputable def DescriptiveComplexity.pullMeanGuard {L : FirstOrder.Language} (X : ExpExpansion L) (C : SOBlock) : (pullLang X C).Sentence

The meaning guard, in the vocabulary of the whole block.

Equations

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

def DescriptiveComplexity.pullMeanPart {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) : (meanBlockB (taggedBlock X)).Assignment (A ⊕ Fin m)

The meaning part of an assignment of the whole block.

Equations

• DescriptiveComplexity.pullMeanPart ρ i = ρ (Sum.inr (Sum.inl i))

theorem DescriptiveComplexity.realize_pullMeanGuard {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) : (A ⊕ Fin m) ⊨ pullMeanGuard X C ↔ (A ⊕ Fin m) ⊨ meanGuardB L (taggedBlock X)

The meaning guard, read in the whole block: it says of the meaning part what DescriptiveComplexity.meanGuardB says.

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

The assignment of the tagged block a point stands for: its own assignment, and the tag bit of its tag alone.

Equations

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

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

Distinct points have distinct assignments: the assignment holds the point's own, and its tag in the tag bits.

theorem DescriptiveComplexity.pullTags_meaning {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (v : A ⊕ Fin m) (t : X.Tag) (ts : Fin ((taggedBlock X).arity (Sum.inr t)) → A ⊕ Fin m) : pullTags ρ v t ↔ meaningOfB (pullMeanPart ρ) (Sum.inr t) v ts

A tag atom is the meaning relation of a nullary variable.

theorem DescriptiveComplexity.pullMeans_inr {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (k : Fin m) (i : X.B.ι) (ts : Fin (X.B.arity i) → A) : pullMeans ρ (Sum.inr k) i ts ↔ meanAtB (pullMeanPart ρ) k ⟨Sum.inl i, ts⟩

theorem DescriptiveComplexity.pullTags_inr {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (k : Fin m) (t : X.Tag) (ts : Fin ((taggedBlock X).arity (Sum.inr t)) → A) : pullTags ρ (Sum.inr k) t ↔ meanAtB (pullMeanPart ρ) k ⟨Sum.inr t, ts⟩

noncomputable def DescriptiveComplexity.pullName {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (hbij : Function.Bijective (meanAtB (pullMeanPart ρ))) (p : X.Map A) : A ⊕ Fin m

The value naming a point: the one whose meaning is the point's assignment, tag bit included.

Equations

• DescriptiveComplexity.pullName ρ hbij p = Sum.inr ((DescriptiveComplexity.meanAssignEquiv (DescriptiveComplexity.pullMeanPart ρ) hbij).symm (DescriptiveComplexity.pointAssign p))

theorem DescriptiveComplexity.meanAtB_symm {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [Finite A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (hbij : Function.Bijective (meanAtB (pullMeanPart ρ))) (α : (taggedBlock X).Assignment A) (i : (taggedBlock X).ι) (ts : Fin ((taggedBlock X).arity i) → A) : meanAtB (pullMeanPart ρ) ((meanAssignEquiv (pullMeanPart ρ) hbij).symm α) ⟨i, ts⟩ ↔ α i ts

theorem DescriptiveComplexity.pullPointRep {L : FirstOrder.Language} {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {m : ℕ} (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (hbij : Function.Bijective (meanAtB (pullMeanPart ρ))) (hshaped : ∀ (i : (taggedBlock X).ι) (v : A ⊕ Fin m) (w : Fin ((taggedBlock X).arity i) → A ⊕ Fin m), meaningOfB (pullMeanPart ρ) i v w → ¬IsOld v ∧ ∀ (j : Fin ((taggedBlock X).arity i)), IsOld (w j)) : PointRep ρ (pullName ρ hbij)

The naming is a representation: it is injective, a point's value means its assignment and carries its tag alone, and – given that a meaning relates an invented value to original elements only – every value that is a point is named.

The sentence, and what an assignment satisfying it gives

noncomputable def DescriptiveComplexity.pullSentence {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (C : SOBlock) (φ : (X.E.sum C.lang).Sentence) : (pullLang X C).Sentence

The sentence: the order guard, the meaning guard, and the translated kernel.

Equations

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

theorem DescriptiveComplexity.pullSentence_back {L : FirstOrder.Language} [L.IsRelational] {X : ExpExpansion L} {C : SOBlock} {A : Type} [L.Structure A] [Finite A] {m : ℕ} (φ : (X.E.sum C.lang).Sentence) (ρ : (pullBlock X C).Assignment (A ⊕ Fin m)) (hψ : (A ⊕ Fin m) ⊨ pullSentence X C φ) : ∃ (inst : LinearOrder A) (σ : C.Assignment (X.Map A)), X.Map A ⊨ φ

From an assignment to the expansion: an assignment satisfying the sentence carries a linear order of the instance and an assignment of the source problem's block over the expansion at that order, for which the source kernel holds.