Exponential expansions that see no order

DescriptiveComplexity.ExpExpansion reads its domain and defining sentences over the ordered expansion of the base vocabulary, and DescriptiveComplexity.ExpDefinable asks for the equivalence at every linear order of the instance. That is why DescriptiveComplexity.EXPTIME and DescriptiveComplexity.EXPSPACE are written SO(≤, LFP) and SO(≤, PFP).

This file introduces the order-free notion – an expansion whose sentences live over the bare vocabulary, so that its universe is defined on a structure carrying no order at all – and proves the easy half of the comparison: an order-free expansion is an expansion, its sentences simply never mentioning the order symbol (DescriptiveComplexity.ExpExpansionFree.toExp), and its expanded structure is the same one (DescriptiveComplexity.ExpExpansionFree.toExpLEquiv), whence DescriptiveComplexity.ExpDefinableFree.expDefinable.

It then builds the converse construction: the order is guessed into the block, as DescriptiveComplexity.sotcDefinable_iff_free guesses it into the state of a walk. DescriptiveComplexity.ExpExpansion.orderFree adds one binary variable to the block, guards it to be a linear order in the domain sentence, reads every defining sentence through it, and requires all the arguments of a symbol to carry the same order. The obstruction this leaves is that the expanded universe becomes the disjoint union, over the linear orders of the instance, of copies of the intended one; the copies are the classes of the new symbol DescriptiveComplexity.ExpExpansion.sameSym, and each is the expanded universe at the order it carries (DescriptiveComplexity.ExpExpansion.copyIn, DescriptiveComplexity.ExpExpansion.exists_copyIn). Reading the inner problem inside one of them is DescriptiveComplexity.Exponential.FreeCopy; staying inside the class while doing so is DescriptiveComplexity.Exponential.FreeSpace for PSPACE, which guesses the copy as a relation, and DescriptiveComplexity.Exponential.FreeTime for PTIME, which names it by one of its points. They conclude EXPSPACE = SO(PFP) and EXPTIME = SO(LFP), with no order in either statement.

The data

structure DescriptiveComplexity.ExpExpansionFree (L : FirstOrder.Language) : Type 1

An order-free exponential expansion: as DescriptiveComplexity.ExpExpansion, except that the domain sentence and the defining sentences live over the bare vocabulary expanded by copies of the block, with no order symbol available. Its universe is therefore defined on a structure carrying no order.

• Tag : Type

  The tags: finitely many copies of the space of block assignments.

• tagFinite : Finite self.Tag

  Tags are finite, so that finite structures expand to finite structures.

• B : SOBlock

  The block whose assignments are the points of the expanded universe.

• E : FirstOrder.Language

  The vocabulary of the expanded structure.

• eRelational : self.E.IsRelational

  The expanded vocabulary is relational, as every vocabulary of this library.

• dom : self.Tag → (L.sum self.B.lang).Sentence

  The domain sentence of each tag, over the bare vocabulary.

• relSentence {n : ℕ} : self.E.Relations n → (Fin n → self.Tag) → (L.sum (self.B.replicate n).lang).Sentence

  The defining sentence of each relation symbol at each tuple of tags, over the bare vocabulary and as many copies of the block as the symbol has arguments.

• dom_nonempty (A : Type) [L.Structure A] [Finite A] [Nonempty A] : ∃ (t : self.Tag) (ρ : self.B.Assignment A), A ⊨ self.dom t

  The definable domain is inhabited.

The expanded universe

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansionFree.Point {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) : Type

A candidate point: a tagged assignment of the block.

Equations

• X.Point A = (X.Tag × X.B.Assignment A)

def DescriptiveComplexity.ExpExpansionFree.DomHolds {L : FirstOrder.Language} {X : ExpExpansionFree L} {A : Type} [L.Structure A] (p : X.Point A) : Prop

The domain condition on a candidate point.

Equations

• DescriptiveComplexity.ExpExpansionFree.DomHolds p = A ⊨ X.dom p.1

def DescriptiveComplexity.ExpExpansionFree.Map {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) [L.Structure A] : Type

The expanded universe: the tagged block assignments satisfying their tag's domain sentence. No order on A is involved.

Equations

• X.Map A = { p : X.Point A // DescriptiveComplexity.ExpExpansionFree.DomHolds p }

theorem DescriptiveComplexity.ExpExpansionFree.map_ext {L : FirstOrder.Language} {X : ExpExpansionFree L} {A : Type} [L.Structure A] {x y : X.Map A} (h₁ : (↑x).1 = (↑y).1) (h₂ : (↑x).2 = (↑y).2) : x = y

Two points of the expanded universe are equal as soon as their tags and their assignments are.

@[instance_reducible]

instance DescriptiveComplexity.ExpExpansionFree.mapStructure {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) [L.Structure A] : X.E.Structure (X.Map A)

The expanded structure.

Equations

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

theorem DescriptiveComplexity.ExpExpansionFree.relMap_map {L : FirstOrder.Language} (X : ExpExpansionFree L) {A : Type} [L.Structure A] {n : ℕ} (r : X.E.Relations n) (xs : Fin n → X.Map A) : FirstOrder.Language.Structure.RelMap r xs ↔ A ⊨ X.relSentence r fun (i : Fin n) => (↑(xs i)).1

instance DescriptiveComplexity.ExpExpansionFree.mapFinite {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) [L.Structure A] [Finite A] : Finite (X.Map A)

instance DescriptiveComplexity.ExpExpansionFree.mapNonempty {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) [L.Structure A] [Finite A] [Nonempty A] : Nonempty (X.Map A)

An order-free expansion is an expansion

def DescriptiveComplexity.ExpExpansionFree.toExp {L : FirstOrder.Language} (X : ExpExpansionFree L) : ExpExpansion L

The same expansion, with the order symbol inserted into every sentence and never used.

Equations

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

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

The two domain conditions agree: the order is inserted and never read.

def DescriptiveComplexity.ExpExpansionFree.toExpEquiv {L : FirstOrder.Language} {X : ExpExpansionFree L} {A : Type} [L.Structure A] [LinearOrder A] : X.toExp.Map A ≃ X.Map A

The two expanded universes are the same set.

Equations

• DescriptiveComplexity.ExpExpansionFree.toExpEquiv = Equiv.subtypeEquivRight ⋯

@[instance_reducible]

def DescriptiveComplexity.ExpExpansionFree.toExpStructure {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) [L.Structure A] [LinearOrder A] : X.E.Structure (X.toExp.Map A)

The expanded structure of DescriptiveComplexity.ExpExpansionFree.toExp – equal to the order-free one by definition, but not syntactically, so instance search has to be handed it.

Equations

• X.toExpStructure A = X.toExp.mapStructure A

def DescriptiveComplexity.ExpExpansionFree.toExpLEquiv {L : FirstOrder.Language} (X : ExpExpansionFree L) (A : Type) [L.Structure A] [LinearOrder A] : X.E.Equiv (X.toExp.Map A) (X.Map A)

The two expanded structures are the same structure: the order-free expansion, read as an ordinary one, interprets every symbol as it did.

Equations

• X.toExpLEquiv A = { toEquiv := DescriptiveComplexity.ExpExpansionFree.toExpEquiv, map_fun' := ⋯, map_rel' := ⋯ }

Order-free definability over an expanded universe

def DescriptiveComplexity.ExpDefinableFree {L : FirstOrder.Language} [L.IsRelational] (C : ComplexityClass) (P : DecisionProblem L) : Prop

Order-free definability over an expanded universe: the problem P holds of A exactly when a fixed Q ∈ C holds of X.Map A, for an expansion whose sentences see no order – so the equivalence is asked of structures carrying no order at all.

Equations

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

theorem DescriptiveComplexity.ExpDefinableFree.expDefinable {L : FirstOrder.Language} [L.IsRelational] {C : ComplexityClass} {P : DecisionProblem L} (h : ExpDefinableFree C P) : ExpDefinable C P

Order-free definability is definability: the easy half of the comparison. The order-free expansion is read as an ordinary one, and its expanded structure is the same, so the same Q witnesses both.

Eliminating the order at n copies of a block

DescriptiveComplexity.orderElimLHom and DescriptiveComplexity.orderElimTwoLHom replace the order symbol by a block's order variable at one and at two copies, which is what an DescriptiveComplexity.SOTCSpec needs. An expansion's defining sentences live over DescriptiveComplexity.SOBlock.replicate n instead, so they need the n-copy analogue: the order is read in the copy k, and each original variable of a copy becomes that copy's variable of the extended block.

def DescriptiveComplexity.orderElimRepLHom (L : FirstOrder.Language) (B : SOBlock) {n : ℕ} (k : Fin n) : (L.sum FirstOrder.Language.order).sum (B.replicate n).lang →ᴸ L.sum (B.withOrder.replicate n).lang

The language morphism eliminating the order symbol over n copies of a block: the order is read in the copy k.

Equations

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

theorem DescriptiveComplexity.orderElimRepLHom_isExpansionOn {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} {k : Fin n} {A : Type} (instA : L.Structure A) (lo : LinearOrder A) (ρs : Fin n → B.withOrder.Assignment A) (hord : ∀ (w : Fin 2 → A), ρs k (Sum.inl ()) w ↔ w 0 ≤ w 1) : (orderElimRepLHom L B k).IsExpansionOn A

The n-copy elimination is an expansion, when the copy k assigns the structure's own order to its order variable.

theorem DescriptiveComplexity.realize_orderElimRep {L : FirstOrder.Language} {B : SOBlock} {n : ℕ} {k : Fin n} {A : Type} (instA : L.Structure A) (lo : LinearOrder A) (ρs : Fin n → B.withOrder.Assignment A) (hord : ∀ (w : Fin 2 → A), ρs k (Sum.inl ()) w ↔ w 0 ≤ w 1) (φ : ((L.sum FirstOrder.Language.order).sum (B.replicate n).lang).Sentence) : A ⊨ (orderElimRepLHom L B k).onSentence φ ↔ A ⊨ φ

The n-copy elimination is correct: a sentence over the ordered expansion and n copies of a block says, read through DescriptiveComplexity.orderElimRepLHom at assignments whose copy k holds the order, what it said of the underlying assignments.

The nullary symbols, shifted to arity one

A defining sentence of a nullary symbol has no copy of the block to read a guessed order from, so an order-guessing expansion cannot define one. It defines the unary shift of the symbol instead: a symbol whose single argument names the point – hence the copy – the value is read in. The vocabulary carrying those shifts is DescriptiveComplexity.nullShiftLang, and DescriptiveComplexity.rep0LHom is what places a nullary sentence in the one copy the shift provides.

inductive DescriptiveComplexity.nullShiftRel (T : Type) : ℕ → Type

Relation symbols of the nullary-shift vocabulary: one unary symbol per nullary symbol of E.

• shift {T : Type} : T → nullShiftRel T 1

  The nullary symbol s, read at arity one.

def DescriptiveComplexity.nullShiftLang (E : FirstOrder.Language) : FirstOrder.Language

The vocabulary carrying the nullary symbols of E at arity one.

Equations

• DescriptiveComplexity.nullShiftLang E = { Functions := fun (x : ℕ) => Empty, Relations := DescriptiveComplexity.nullShiftRel (E.Relations 0) }

instance DescriptiveComplexity.instIsRelationalNullShiftLang (E : FirstOrder.Language) : (nullShiftLang E).IsRelational

def DescriptiveComplexity.rep01Hom (B : SOBlock) : (B.replicate 0).ι → (B.replicate 1).ι

The map of relation variables placing no copy of a block inside one copy. Its source is empty, so there is nothing to choose.

Equations

• DescriptiveComplexity.rep01Hom B p = (0, p.2)

theorem DescriptiveComplexity.rep01Hom_arity (B : SOBlock) (i : (B.replicate 0).ι) : (B.replicate 1).arity (rep01Hom B i) = (B.replicate 0).arity i

def DescriptiveComplexity.rep0LHom (L₀ : FirstOrder.Language) (B : SOBlock) : L₀.sum (B.replicate 0).lang →ᴸ L₀.sum (B.replicate 1).lang

Reading a sentence over no copy of a block inside one copy – the shape a nullary defining sentence has, placed where the order can be read.

Equations

• DescriptiveComplexity.rep0LHom L₀ B = (FirstOrder.Language.LHom.id L₀).sumMap (DescriptiveComplexity.SOBlock.homLHom (DescriptiveComplexity.rep01Hom B) ⋯)

theorem DescriptiveComplexity.replicate_zero_assign_eq {B : SOBlock} {A : Type} (ρ σ : (B.replicate 0).Assignment A) : ρ = σ

Any two assignments of a block replicated zero times agree: the index type is empty.

theorem DescriptiveComplexity.realize_rep0LHom {L₀ : FirstOrder.Language} {B : SOBlock} {A : Type} [inst : L₀.Structure A] (σ : (B.replicate 1).Assignment A) (σ₀ : (B.replicate 0).Assignment A) (φ : (L₀.sum (B.replicate 0).lang).Sentence) : A ⊨ (rep0LHom L₀ B).onSentence φ ↔ A ⊨ φ

Placing a nullary sentence in one copy is correct: it says there what it said with no copy at all.

Guessing the order into the block

The hard direction, at the level of the expansion. The block is extended by one binary variable, the domain sentence guards it to be a linear order and reads the old domain through it, and every defining sentence requires all of its arguments to carry the same order before reading the old sentence through the first of them. The expanded universe becomes the disjoint union, over the linear orders of the instance, of copies of the intended one, and the new binary symbol same marks the copies.

A nullary symbol of the original vocabulary has no copy of the block to read an order from, so the guessing expansion cannot define it: it defines its unary shift instead (DescriptiveComplexity.nullShiftLang), whose one argument names the copy the value is read in, and leaves the nullary symbol itself at ⊥. Nothing is lost – a reader of the expanded structure finds the value of a nullary symbol inside a copy where the shift holds – and the construction needs no hypothesis on the arities.

inductive DescriptiveComplexity.sameRel : ℕ → Type

Relation symbols of the same-order vocabulary: one binary symbol.

• same : sameRel 2

  same x y: the points x and y carry the same guessed order.

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

Equations

• DescriptiveComplexity.instDecidableEqSameRel.decEq DescriptiveComplexity.sameRel.same DescriptiveComplexity.sameRel.same = isTrue DescriptiveComplexity.instDecidableEqSameRel.decEq._proof_1

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSameRel {a✝ : ℕ} : DecidableEq (sameRel a✝)

Equations

• DescriptiveComplexity.instDecidableEqSameRel = DescriptiveComplexity.instDecidableEqSameRel.decEq

def DescriptiveComplexity.sameLang : FirstOrder.Language

The vocabulary of a single binary symbol, marking the points of an order-guessing expansion that carry the same order.

Equations

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

instance DescriptiveComplexity.instIsRelationalSameLang : sameLang.IsRelational

@[reducible, inline]

abbrev DescriptiveComplexity.ordCopySym (B : SOBlock) {n : ℕ} (j : Fin n) : (B.withOrder.replicate n).lang.Relations 2

The order variable of the copy j, as a symbol of the replicated vocabulary.

Equations

• DescriptiveComplexity.ordCopySym B j = ⟨(j, Sum.inl ()), ⋯⟩

noncomputable def DescriptiveComplexity.ordAgreeS (L : FirstOrder.Language) (B : SOBlock) {n : ℕ} (j : Fin (n + 1)) : (L.sum (B.withOrder.replicate (n + 1)).lang).Sentence

The copies 0 and j carry the same order.

Equations

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

noncomputable def DescriptiveComplexity.allSameOrdS (L : FirstOrder.Language) (B : SOBlock) (n : ℕ) : (L.sum (B.withOrder.replicate (n + 1)).lang).Sentence

All the copies carry the same order.

Equations

• DescriptiveComplexity.allSameOrdS L B n = DescriptiveComplexity.listInf (List.map (DescriptiveComplexity.ordAgreeS L B) (List.finRange (n + 1)))

theorem DescriptiveComplexity.realize_allSameOrdS {L : FirstOrder.Language} {B : SOBlock} {A : Type} [L.Structure A] {n : ℕ} (ρs : Fin (n + 1) → B.withOrder.Assignment A) : A ⊨ allSameOrdS L B n ↔ ∀ (j : Fin (n + 1)) (w : Fin 2 → A), ρs 0 (Sum.inl ()) w ↔ ρs j (Sum.inl ()) w

The order-guessing expansion

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

The order, guessed into the block: the same expansion with one binary variable added, its domain sentence guarding that variable to be a linear order and reading the old domain through it, and each defining sentence requiring all of its arguments to carry the same order before reading the old sentence through the first of them. A nullary symbol keeps no value – it has no copy to read the order in – and its content moves to its unary shift, read in the copy its argument names.

Equations

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

The symbols of the order-guessing vocabulary

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.origSym {L : FirstOrder.Language} (X : ExpExpansion L) {n : ℕ} (r : X.E.Relations n) : X.orderFree.E.Relations n

A relation symbol of the original vocabulary, read in the order-guessing one.

Equations

• X.origSym r = Sum.inl (Sum.inl r)

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.nullSym {L : FirstOrder.Language} (X : ExpExpansion L) (s : X.E.Relations 0) : X.orderFree.E.Relations 1

The unary shift of a nullary symbol of the original vocabulary: it holds of the points of a copy exactly when the symbol held in that copy.

Equations

• X.nullSym s = Sum.inl (Sum.inr (DescriptiveComplexity.nullShiftRel.shift s))

@[reducible, inline]

abbrev DescriptiveComplexity.ExpExpansion.sameSym {L : FirstOrder.Language} (X : ExpExpansion L) : X.orderFree.E.Relations 2

The symbol marking two points that carry the same guessed order.

Equations

• X.sameSym = Sum.inr DescriptiveComplexity.sameRel.same

The guessed order of a point

Everything in this section is stated on a structure carrying no order: it is what a reader of the order-guessing expansion sees.

def DescriptiveComplexity.ExpExpansion.pointOrd {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] (p : X.orderFree.Map A) : (Fin 2 → A) → Prop

The order a point carries: the value of the guessed order variable in its assignment.

Equations

• DescriptiveComplexity.ExpExpansion.pointOrd p = (↑p).2 (Sum.inl ())

theorem DescriptiveComplexity.ExpExpansion.relMap_sameSym {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] (xs : Fin 2 → X.orderFree.Map A) : FirstOrder.Language.Structure.RelMap X.sameSym xs ↔ ∀ (w : Fin 2 → A), pointOrd (xs 0) w ↔ pointOrd (xs 1) w

The same symbol compares the guessed orders.

theorem DescriptiveComplexity.ExpExpansion.pointOrd_linear {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] (p : X.orderFree.Map A) : (∀ (a : A), pointOrd p ![a, a]) ∧ (∀ (a b c : A), pointOrd p ![a, b] → pointOrd p ![b, c] → pointOrd p ![a, c]) ∧ (∀ (a b : A), pointOrd p ![a, b] → pointOrd p ![b, a] → a = b) ∧ ∀ (a b : A), pointOrd p ![a, b] ∨ pointOrd p ![b, a]

The guessed order of a point satisfies the linear-order axioms: its domain sentence guards it.

@[instance_reducible]

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

The linear order a point carries.

Equations

• DescriptiveComplexity.ExpExpansion.guessedLinearOrder p = DescriptiveComplexity.linearOrderOfGuard (DescriptiveComplexity.ExpExpansion.pointOrd p) ⋯ ⋯ ⋯ ⋯

theorem DescriptiveComplexity.ExpExpansion.le_guessedLinearOrder {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] (p : X.orderFree.Map A) (w : Fin 2 → A) : w 0 ≤ w 1 ↔ pointOrd p w

def DescriptiveComplexity.ExpExpansion.loRel {A : Type} [LinearOrder A] : (Fin 2 → A) → Prop

The ambient order, as a binary relation on tuples.

Equations

• DescriptiveComplexity.ExpExpansion.loRel w = (w 0 ≤ w 1)

theorem DescriptiveComplexity.ExpExpansion.domHolds_copyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (x : X.Map A) : ExpExpansionFree.DomHolds ((↑x).1, X.B.joinOrder loRel (↑x).2)

The guessed order of a placed point is the ambient one.

def DescriptiveComplexity.ExpExpansion.copyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (x : X.Map A) : X.orderFree.Map A

A point of the expansion, placed in the copy of the ambient order.

Equations

• DescriptiveComplexity.ExpExpansion.copyIn x = ⟨((↑x).1, X.B.joinOrder DescriptiveComplexity.ExpExpansion.loRel (↑x).2), ⋯⟩

@[simp]

theorem DescriptiveComplexity.ExpExpansion.copyIn_tag {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (x : X.Map A) : (↑(copyIn x)).1 = (↑x).1

@[simp]

theorem DescriptiveComplexity.ExpExpansion.copyIn_rest {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (x : X.Map A) : X.B.restPart (↑(copyIn x)).2 = (↑x).2

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

theorem DescriptiveComplexity.ExpExpansion.pointOrd_copyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (x : X.Map A) (w : Fin 2 → A) : pointOrd (copyIn x) w ↔ w 0 ≤ w 1

The guessed order of a placed point is the ambient one.

theorem DescriptiveComplexity.ExpExpansion.relMap_copyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {m : ℕ} (r : X.E.Relations (m + 1)) (xs : Fin (m + 1) → X.Map A) : (FirstOrder.Language.Structure.RelMap (X.origSym r) fun (i : Fin (m + 1)) => copyIn (xs i)) ↔ FirstOrder.Language.Structure.RelMap r xs

The relations are unchanged inside a copy: a relation of the original vocabulary, of arity at least one, holds of points of one copy exactly when it held of them.

theorem DescriptiveComplexity.ExpExpansion.relMap_nullCopyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] (s : X.E.Relations 0) (xs : Fin 1 → X.Map A) (ys : Fin 0 → X.Map A) : (FirstOrder.Language.Structure.RelMap (X.nullSym s) fun (i : Fin 1) => copyIn (xs i)) ↔ FirstOrder.Language.Structure.RelMap s ys

The unary shift carries the nullary symbols inside a copy: it holds of a placed point exactly when the nullary symbol held.

Reading a copy back

The converse of DescriptiveComplexity.ExpExpansion.copyIn: a point whose guessed order is the ambient one is a placed point, so the copies of the order-guessing expansion are exactly the images of the copy maps, one per linear order of the instance.

theorem DescriptiveComplexity.ExpExpansion.joinOrder_restPart {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [LinearOrder A] {ρ : X.B.withOrder.Assignment A} (hord : ∀ (w : Fin 2 → A), ρ (Sum.inl ()) w ↔ loRel w) : X.B.joinOrder loRel (X.B.restPart ρ) = ρ

Rebuilding an assignment from its order variable and the rest.

theorem DescriptiveComplexity.ExpExpansion.domHolds_of_pointOrd {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {p : X.orderFree.Map A} (hord : ∀ (w : Fin 2 → A), pointOrd p w ↔ loRel w) : DomHolds ((↑p).1, X.B.restPart (↑p).2)

The domain condition survives reading a point back at the order it carries.

theorem DescriptiveComplexity.ExpExpansion.exists_copyIn {L : FirstOrder.Language} {X : ExpExpansion L} {A : Type} [L.Structure A] [LinearOrder A] {p : X.orderFree.Map A} (hord : ∀ (w : Fin 2 → A), pointOrd p w ↔ loRel w) : ∃ (x : X.Map A), copyIn x = p

A point carrying the ambient order is a placed point.