The canonical order is inflationary-definable

That one fixed-point formula orders the ≡ᵏ-classes uniformly over all finite structures is the central lemma of Dawar–Lindell–Weinstein 1995; here it is stated as the first-order definition of the ordered pebble refinement (DescriptiveComplexity.Invariant.OrderedPebble): a simultaneous induction DescriptiveComplexity.ordStepDef over the base vocabulary, with one relation variable of arity k + k holding the current strict order on k-tuples, whose inflationary stages are exactly the stages of the ordered refinement (DescriptiveComplexity.inflStage_ordStepDef), so whose limit is the canonical order DescriptiveComplexity.OrdK on the ≡ᵏ-classes.

The initial coloring is the atomic bit vector relative to a finite agreement family S (DescriptiveComplexity.atomColor): one bit per coordinate equality and one per relation of S at each selection of coordinates, ordered lexicographically along an arbitrary enumeration of the bits. Its agreement is atomic agreement (DescriptiveComplexity.colorAgree_atomColor), which plugs the definable order into the invariant structure's linear order (DescriptiveComplexity.invLinearOrder).

Every piece of one refinement round is written as a first-order formula over the expanded vocabulary – the bit comparisons as finite lexicographic disjunctions, membership in a move set with one quantifier, move-set comparison with a quantified separating tuple and a quantified minimality check – and each formula builder comes with its realization lemma, so the step formula realizes one round of DescriptiveComplexity.ordRefine (DescriptiveComplexity.realize_ordStepF).

The order block and its symbol

@[reducible]

def DescriptiveComplexity.ordBlock (k : ℕ) : SOBlock

The block of the definable refinement: one relation variable of arity k + k, the current strict order on k-tuples.

Equations

• DescriptiveComplexity.ordBlock k = { ι := Unit, ιFinite := ⋯, arity := fun (x : Unit) => k + k }

@[reducible, inline]

abbrev DescriptiveComplexity.ordVSym (L : FirstOrder.Language) (k : ℕ) : (L.sum (ordBlock k).lang).Relations (k + k)

The order variable's relation symbol.

Equations

• DescriptiveComplexity.ordVSym L k = Sum.inr ⟨(), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ordBaseSym (L : FirstOrder.Language) (k : ℕ) {l : ℕ} (R : L.Relations l) : (L.sum (ordBlock k).lang).Relations l

A base relation symbol, in the vocabulary expanded by the order block.

Equations

• DescriptiveComplexity.ordBaseSym L k R = Sum.inl R

def DescriptiveComplexity.toPebble {k : ℕ} {A : Type} (σ : (ordBlock k).Assignment A) : PebbleRel A k

The strict order on k-tuples held by an assignment of the order block.

Equations

• DescriptiveComplexity.toPebble σ u v = σ () fun (i : Fin (k + k)) => Fin.addCases u v i

theorem DescriptiveComplexity.addCases_comp {k : ℕ} {A γ : Type} (w : γ → A) (f g : Fin k → γ) : (fun (i : Fin (k + k)) => Fin.addCases (fun (i : Fin k) => w (f i)) (fun (i : Fin k) => w (g i)) i) = fun (p : Fin (k + k)) => w (Fin.addCases f g p)

Reading a k + k-tuple as two k-tuples.

Formula builders

Each builder takes the tuples it speaks about as selections of variables Fin k → γ in an arbitrary context γ, so that the builders compose under the quantifiers Formula.iExs/Formula.iAlls.

noncomputable def DescriptiveComplexity.ordPrecF (L : FirstOrder.Language) (k : ℕ) {γ : Type} (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

The ≺-atom between two k-tuples of variables.

Equations

• DescriptiveComplexity.ordPrecF L k f g = (DescriptiveComplexity.ordVSym L k).formula fun (p : Fin (k + k)) => FirstOrder.Language.var (Fin.addCases f g p)

noncomputable def DescriptiveComplexity.incompF (L : FirstOrder.Language) (k : ℕ) {γ : Type} (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Incomparability of two k-tuples of variables.

Equations

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

noncomputable def DescriptiveComplexity.inMovesF (L : FirstOrder.Language) (k : ℕ) {γ : Type} [DecidableEq γ] (j : Fin k) (f x : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Membership of the class of x in the move set of f at pebble j: some value of pebble j moves f into the class of x.

Equations

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

noncomputable def DescriptiveComplexity.movesDiffF (L : FirstOrder.Language) (k : ℕ) {γ : Type} [DecidableEq γ] (j : Fin k) (f g x : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

The class of x separates the move sets of f and g at pebble j.

Equations

• DescriptiveComplexity.movesDiffF L k j f g x = FirstOrder.Language.BoundedFormula.not ((DescriptiveComplexity.inMovesF L k j f x).iff (DescriptiveComplexity.inMovesF L k j g x))

noncomputable def DescriptiveComplexity.setLessF (L : FirstOrder.Language) (k : ℕ) {γ : Type} [DecidableEq γ] (j : Fin k) (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Move-set comparison at pebble j: some separating class in the move set of f and not of g is minimal among the separating classes.

Equations

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

noncomputable def DescriptiveComplexity.movesEqF (L : FirstOrder.Language) (k : ℕ) {γ : Type} [DecidableEq γ] (j : Fin k) (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Move-set equality at pebble j.

Equations

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

noncomputable def DescriptiveComplexity.movesLessF (L : FirstOrder.Language) (k : ℕ) {γ : Type} [DecidableEq γ] (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Lexicographic move-set comparison over the pebbles.

Equations

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

Realization of the builders

theorem DescriptiveComplexity.realize_ordPrecF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} (f g : Fin k → γ) (w : γ → A) : (ordPrecF L k f g).Realize w ↔ toPebble σ (fun (i : Fin k) => w (f i)) fun (i : Fin k) => w (g i)

theorem DescriptiveComplexity.realize_incompF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} (f g : Fin k → γ) (w : γ → A) : (incompF L k f g).Realize w ↔ IncompRel (toPebble σ) (fun (i : Fin k) => w (f i)) fun (i : Fin k) => w (g i)

theorem DescriptiveComplexity.realize_inMovesF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} [DecidableEq γ] (j : Fin k) (f x : Fin k → γ) (w : γ → A) : (inMovesF L k j f x).Realize w ↔ InMoves (toPebble σ) j (fun (i : Fin k) => w (f i)) fun (i : Fin k) => w (x i)

theorem DescriptiveComplexity.realize_movesDiffF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} [DecidableEq γ] (j : Fin k) (f g x : Fin k → γ) (w : γ → A) : (movesDiffF L k j f g x).Realize w ↔ MovesDiff (toPebble σ) j (fun (i : Fin k) => w (f i)) (fun (i : Fin k) => w (g i)) fun (i : Fin k) => w (x i)

theorem DescriptiveComplexity.realize_setLessF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} [DecidableEq γ] (j : Fin k) (f g : Fin k → γ) (w : γ → A) : (setLessF L k j f g).Realize w ↔ SetLess (toPebble σ) j (fun (i : Fin k) => w (f i)) fun (i : Fin k) => w (g i)

theorem DescriptiveComplexity.realize_movesEqF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} [DecidableEq γ] (j : Fin k) (f g : Fin k → γ) (w : γ → A) : (movesEqF L k j f g).Realize w ↔ MovesEq (toPebble σ) j (fun (i : Fin k) => w (f i)) fun (i : Fin k) => w (g i)

theorem DescriptiveComplexity.realize_movesLessF {L : FirstOrder.Language} {k : ℕ} {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} [DecidableEq γ] (f g : Fin k → γ) (w : γ → A) : (movesLessF L k f g).Realize w ↔ MovesLess (toPebble σ) (fun (i : Fin k) => w (f i)) fun (i : Fin k) => w (g i)

The atomic bit coloring

@[reducible]

def DescriptiveComplexity.BitIdx (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) : Type

The bit positions of the atomic coloring: one per coordinate equality, one per relation of the family at each selection of coordinates.

Equations

• DescriptiveComplexity.BitIdx L k S = (Fin k × Fin k ⊕ (R : ↑S) × (Fin (↑R).fst → Fin k))

noncomputable def DescriptiveComplexity.atomBits (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] (w : Fin k → A) : BitIdx L k S → Bool

The atomic bit vector of a k-tuple.

Equations

• DescriptiveComplexity.atomBits L k S w (Sum.inl (i, j)) = decide (w i = w j)
• DescriptiveComplexity.atomBits L k S w (Sum.inr ⟨R, gsel⟩) = decide (FirstOrder.Language.Structure.RelMap (↑R).snd fun (p : Fin (↑R).fst) => w (gsel p))

noncomputable def DescriptiveComplexity.atomColor (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] (w : Fin k → A) : Lex (BitIdx L k S → Bool)

The atomic coloring: the bit vector, compared lexicographically.

Equations

• DescriptiveComplexity.atomColor L k S w = toLex (DescriptiveComplexity.atomBits L k S w)

@[instance_reducible]

noncomputable def DescriptiveComplexity.bitIdxLinearOrder (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) (hS : S.Finite) : LinearOrder (BitIdx L k S)

An arbitrary enumeration order on the bit positions (finitely many, for a finite family).

Equations

• DescriptiveComplexity.bitIdxLinearOrder L k S hS = DescriptiveComplexity.finiteLinearOrder (DescriptiveComplexity.BitIdx L k S)

@[instance_reducible]

noncomputable def DescriptiveComplexity.bitVecLinearOrder (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) (hS : S.Finite) : LinearOrder (Lex (BitIdx L k S → Bool))

The lexicographic order on bit vectors.

Equations

• DescriptiveComplexity.bitVecLinearOrder L k S hS = inferInstance

theorem DescriptiveComplexity.colorAgree_atomColor (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] : colorAgree (atomColor L k S) = atomicAgreeOn S A k

The agreement of the atomic coloring is atomic agreement.

The bit comparison formulas

noncomputable def DescriptiveComplexity.atomBitF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {γ : Type} (b : BitIdx L k S) (f : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

The formula of one atomic bit at a selection of variables.

Equations

• DescriptiveComplexity.atomBitF L k S (Sum.inl (i, j)) f = (FirstOrder.Language.var (f i)).equal (FirstOrder.Language.var (f j))
• DescriptiveComplexity.atomBitF L k S (Sum.inr ⟨R, gsel⟩) f = (DescriptiveComplexity.ordBaseSym L k (↑R).snd).formula fun (p : Fin (↑R).fst) => FirstOrder.Language.var (f (gsel p))

noncomputable def DescriptiveComplexity.atomBitEqF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {γ : Type} (b : BitIdx L k S) (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Bit agreement at two selections of variables.

Equations

• DescriptiveComplexity.atomBitEqF L k S b f g = (DescriptiveComplexity.atomBitF L k S b f).iff (DescriptiveComplexity.atomBitF L k S b g)

noncomputable def DescriptiveComplexity.atomLessF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) (hS : S.Finite) {γ : Type} (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Lexicographic bit-vector comparison: agree before some bit, 0 < 1 at it.

Equations

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

noncomputable def DescriptiveComplexity.atomEqF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) (hS : S.Finite) {γ : Type} (f g : Fin k → γ) : (L.sum (ordBlock k).lang).Formula γ

Bit-vector equality.

Equations

• DescriptiveComplexity.atomEqF L k S hS f g = FirstOrder.Language.Formula.iInf fun (b : DescriptiveComplexity.BitIdx L k S) => DescriptiveComplexity.atomBitEqF L k S b f g

theorem DescriptiveComplexity.realize_atomBitF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} (b : BitIdx L k S) (f : Fin k → γ) (w : γ → A) : (atomBitF L k S b f).Realize w ↔ atomBits L k S (fun (i : Fin k) => w (f i)) b = true

theorem DescriptiveComplexity.realize_atomBitEqF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} {γ : Type} (b : BitIdx L k S) (f g : Fin k → γ) (w : γ → A) : (atomBitEqF L k S b f g).Realize w ↔ atomBits L k S (fun (i : Fin k) => w (f i)) b = atomBits L k S (fun (i : Fin k) => w (g i)) b

theorem DescriptiveComplexity.realize_atomLessF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} (hS : S.Finite) {γ : Type} (f g : Fin k → γ) (w : γ → A) : (atomLessF L k S hS f g).Realize w ↔ (atomColor L k S fun (i : Fin k) => w (f i)) < atomColor L k S fun (i : Fin k) => w (g i)

theorem DescriptiveComplexity.realize_atomEqF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] {σ : (ordBlock k).Assignment A} (hS : S.Finite) {γ : Type} (f g : Fin k → γ) (w : γ → A) : (atomEqF L k S hS f g).Realize w ↔ (atomColor L k S fun (i : Fin k) => w (f i)) = atomColor L k S fun (i : Fin k) => w (g i)

The step formula and the induction

noncomputable def DescriptiveComplexity.ordStepF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) (hS : S.Finite) : (L.sum (ordBlock k).lang).Formula (Fin (k + k))

The step formula of the definable refinement: one round of DescriptiveComplexity.ordRefine, over the current order variable.

Equations

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

noncomputable def DescriptiveComplexity.ordStepDef (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) (hS : S.Finite) : StepDef L

The definable refinement: the simultaneous induction computing the canonical order on k-tuples, inflationarily. (The output sentence is irrelevant: the induction is consumed as the first stratum of a stratification.)

Equations

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

theorem DescriptiveComplexity.realize_ordStepF (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] (hS : S.Finite) {σ : (ordBlock k).Assignment A} (w : Fin (k + k) → A) : (ordStepF L k S hS).Realize w ↔ (IncompRel (toPebble σ) (fun (i : Fin k) => w (Fin.castAdd k i)) fun (i : Fin k) => w (Fin.natAdd k i)) ∧ (((atomColor L k S fun (i : Fin k) => w (Fin.castAdd k i)) < atomColor L k S fun (i : Fin k) => w (Fin.natAdd k i)) ∨ ((atomColor L k S fun (i : Fin k) => w (Fin.castAdd k i)) = atomColor L k S fun (i : Fin k) => w (Fin.natAdd k i)) ∧ MovesLess (toPebble σ) (fun (i : Fin k) => w (Fin.castAdd k i)) fun (i : Fin k) => w (Fin.natAdd k i))

theorem DescriptiveComplexity.inflStage_ordStepDef (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] (hS : S.Finite) (n : ℕ) : (ordStepDef L k S hS).inflStage A n = fun (x : (ordStepDef L k S hS).B.ι) (w : Fin ((ordStepDef L k S hS).B.arity x) → A) => ordStage (atomColor L k S) n (fun (i : Fin k) => w (Fin.castAdd k i)) fun (i : Fin k) => w (Fin.natAdd k i)

The stages of the definable refinement are the stages of the ordered pebble refinement.

theorem DescriptiveComplexity.toPebble_inflLimit_ordStepDef (L : FirstOrder.Language) (k : ℕ) (S : Set ((n : ℕ) × L.Relations n)) {A : Type} [L.Structure A] (hS : S.Finite) : toPebble ((ordStepDef L k S hS).inflLimit A) = OrdK (atomColor L k S)

The value of the definable refinement is the canonical order.