The canonical order on ≡ᵏ-classes, as an inflationary refinement

The k-pebble refinement (DescriptiveComplexity.Invariant.Pebble) splits classes round by round; this file runs the ordered version of the same refinement: a strict order DescriptiveComplexity.ordStage on k-tuples that grows round by round – tuples split apart become comparable, and stay comparable for ever after. The initial data is a coloring c₀ of the tuples in a linear order (over a structure: the atomic type, read as a tuple of bits); one round (DescriptiveComplexity.ordRefine) keeps the current order and, inside one incomparability class, compares first the colors, then the move sets – at the first pebble where they differ, the sets of current classes reachable by moving that pebble, compared through their least separating class (DescriptiveComplexity.SetLess).

The point of the construction, and the reason it is phrased as a growing chain, is twofold:

• its incomparability is exactly the pebble refinement, stage by stage (the third component of DescriptiveComplexity.ordStage_invariant) and at the limit DescriptiveComplexity.OrdK, whose incomparability is ≡ᵏ (DescriptiveComplexity.incompRel_ordK_eq); the limit is asymmetric and transitive (DescriptiveComplexity.ordK_asymm, DescriptiveComplexity.ordK_trans), and total across classes (DescriptiveComplexity.ordK_or_of_not_equivK) by the very definition of incomparability – a canonical linear order on the ≡ᵏ-classes;
• the chain is inflationary, so it is computed by an inflationary fixed-point induction – one more relation variable alongside any other – and its canonicity (invariance under isomorphisms) is inherited from the transport of inflationary stages rather than proved by hand.

Everything is stated over a bare type and an abstract coloring, with no vocabulary in sight, exactly as in DescriptiveComplexity.Invariant.Pebble; the instantiation at the atomic coloring of a structure, and the first-order definition of one round, live with the invariant structure.

Incomparability, move sets, and set comparison

def DescriptiveComplexity.IncompRel {A : Type} {k : ℕ} (O : PebbleRel A k) : PebbleRel A k

Incomparability in a relation on k-tuples: the current classes.

Equations

• DescriptiveComplexity.IncompRel O u v = (¬O u v ∧ ¬O v u)

theorem DescriptiveComplexity.IncompRel.symm {A : Type} {k : ℕ} {O : PebbleRel A k} {u v : Fin k → A} (h : IncompRel O u v) : IncompRel O v u

def DescriptiveComplexity.InMoves {A : Type} {k : ℕ} (O : PebbleRel A k) (j : Fin k) (u x : Fin k → A) : Prop

The class of x belongs to the move set of u at pebble j: some move of pebble j from u lands in the class of x.

Equations

• DescriptiveComplexity.InMoves O j u x = ∃ (a : A), DescriptiveComplexity.IncompRel O (Function.update u j a) x

def DescriptiveComplexity.MovesEq {A : Type} {k : ℕ} (O : PebbleRel A k) (j : Fin k) (u v : Fin k → A) : Prop

The move sets of u and v at pebble j coincide.

Equations

• DescriptiveComplexity.MovesEq O j u v = ∀ (x : Fin k → A), DescriptiveComplexity.InMoves O j u x ↔ DescriptiveComplexity.InMoves O j v x

def DescriptiveComplexity.MovesDiff {A : Type} {k : ℕ} (O : PebbleRel A k) (j : Fin k) (u v x : Fin k → A) : Prop

The class of x separates the move sets of u and v at pebble j.

Equations

• DescriptiveComplexity.MovesDiff O j u v x = ¬(DescriptiveComplexity.InMoves O j u x ↔ DescriptiveComplexity.InMoves O j v x)

theorem DescriptiveComplexity.MovesDiff.symm {A : Type} {k : ℕ} {O : PebbleRel A k} {j : Fin k} {u v x : Fin k → A} (h : MovesDiff O j u v x) : MovesDiff O j v u x

def DescriptiveComplexity.SetLess {A : Type} {k : ℕ} (O : PebbleRel A k) (j : Fin k) (u v : Fin k → A) : Prop

Comparison of move sets at pebble j: a class in the move set of u but not of v is minimal among the separating classes.

Equations

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

def DescriptiveComplexity.MovesLess {A : Type} {k : ℕ} (O : PebbleRel A k) (u v : Fin k → A) : Prop

Lexicographic comparison of the move sets over the pebbles: equal before some pebble, less at it.

Equations

• DescriptiveComplexity.MovesLess O u v = ∃ (j : Fin k), (∀ j' < j, DescriptiveComplexity.MovesEq O j' u v) ∧ DescriptiveComplexity.SetLess O j u v

One round of the ordered refinement, and the chain

def DescriptiveComplexity.colorAgree {A : Type} {k : ℕ} {β : Type u_1} (c₀ : (Fin k → A) → β) : PebbleRel A k

Agreement on the coloring: the initial relation of the refinement.

Equations

• DescriptiveComplexity.colorAgree c₀ u v = (c₀ u = c₀ v)

theorem DescriptiveComplexity.colorAgree_equivalence {A : Type} {k : ℕ} {β : Type u_1} (c₀ : (Fin k → A) → β) : Equivalence (colorAgree c₀)

def DescriptiveComplexity.ordRefine {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) (O : PebbleRel A k) : PebbleRel A k

One round of the ordered refinement: keep the current order; inside one incomparability class, compare the colors, then the move sets.

Equations

• DescriptiveComplexity.ordRefine c₀ O u v = (O u v ∨ DescriptiveComplexity.IncompRel O u v ∧ (c₀ u < c₀ v ∨ c₀ u = c₀ v ∧ DescriptiveComplexity.MovesLess O u v))

def DescriptiveComplexity.ordStage {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) : ℕ → PebbleRel A k

The ordered refinement chain, from the empty order.

Equations

• DescriptiveComplexity.ordStage c₀ 0 = fun (x x_1 : Fin k → A) => False
• DescriptiveComplexity.ordStage c₀ n.succ = DescriptiveComplexity.ordRefine c₀ (DescriptiveComplexity.ordStage c₀ n)

def DescriptiveComplexity.OrdK {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) : PebbleRel A k

The canonical order: the union of the ordered refinement chain. Its incomparability is ≡ᵏ (DescriptiveComplexity.incompRel_ordK_eq), and it is transitive and asymmetric, so it is a linear order on the ≡ᵏ-classes.

Equations

• DescriptiveComplexity.OrdK c₀ u v = ∃ (n : ℕ), DescriptiveComplexity.ordStage c₀ n u v

theorem DescriptiveComplexity.ordStage_le_succ {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) (n : ℕ) {u v : Fin k → A} (h : ordStage c₀ n u v) : ordStage c₀ (n + 1) u v

The chain grows: one round only ever adds pairs.

theorem DescriptiveComplexity.ordStage_le_of_le {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) {m n : ℕ} (hmn : m ≤ n) {u v : Fin k → A} (h : ordStage c₀ m u v) : ordStage c₀ n u v

The chain grows, monotonically.

Structural lemmas

Each lemma of this section holds for any relation with the listed fragments of the stage invariant – asymmetry, transitivity, transitivity of incomparability – which the master induction (DescriptiveComplexity.ordStage_invariant) establishes stage by stage.

theorem DescriptiveComplexity.IncompRel.congr_left {A : Type} {k : ℕ} {O : PebbleRel A k} (htrans : ∀ (u v w : Fin k → A), O u v → O v w → O u w) (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {u v w : Fin k → A} (h : O u v) (hvw : IncompRel O v w) : O u w

Comparability is a congruence for incomparability, on the right.

theorem DescriptiveComplexity.IncompRel.congr_right {A : Type} {k : ℕ} {O : PebbleRel A k} (htrans : ∀ (u v w : Fin k → A), O u v → O v w → O u w) (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {u v w : Fin k → A} (huv : IncompRel O u v) (h : O v w) : O u w

Comparability is a congruence for incomparability, on the left.

theorem DescriptiveComplexity.InMoves.congr {A : Type} {k : ℕ} {O : PebbleRel A k} (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {j : Fin k} {u x y : Fin k → A} (h : InMoves O j u x) (hxy : IncompRel O x y) : InMoves O j u y

Membership in a move set only depends on the class of the target.

theorem DescriptiveComplexity.setLess_or {A : Type} {k : ℕ} {O : PebbleRel A k} (hasymm : ∀ (u v : Fin k → A), O u v → ¬O v u) (htrans : ∀ (u v w : Fin k → A), O u v → O v w → O u w) [Finite A] {j : Fin k} {u v : Fin k → A} (h : ¬MovesEq O j u v) : SetLess O j u v ∨ SetLess O j v u

If the move sets differ, one compares below the other: the least separating class lands on one of the two sides.

theorem DescriptiveComplexity.setLess_asymm {A : Type} {k : ℕ} {O : PebbleRel A k} (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {j : Fin k} {u v : Fin k → A} (h : SetLess O j u v) : ¬SetLess O j v u

Set comparison is asymmetric: the two candidate least separating classes would be incomparable, hence equal as classes, hence on the same side.

theorem DescriptiveComplexity.SetLess.congr_right {A : Type} {k : ℕ} {O : PebbleRel A k} {j : Fin k} {u v w : Fin k → A} (h : SetLess O j u v) (hvw : MovesEq O j v w) : SetLess O j u w

Set comparison is invariant under move-set equality on the right.

theorem DescriptiveComplexity.SetLess.congr_left {A : Type} {k : ℕ} {O : PebbleRel A k} {j : Fin k} {u v w : Fin k → A} (huv : MovesEq O j u v) (h : SetLess O j v w) : SetLess O j u w

Set comparison is invariant under move-set equality on the left.

theorem DescriptiveComplexity.setLess_trans {A : Type} {k : ℕ} {O : PebbleRel A k} (htrans : ∀ (u v w : Fin k → A), O u v → O v w → O u w) (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {j : Fin k} {u v w : Fin k → A} (h₁ : SetLess O j u v) (h₂ : SetLess O j v w) : SetLess O j u w

Set comparison is transitive: compare the two least separating classes, and reuse the smaller one.

theorem DescriptiveComplexity.SetLess.not_movesEq {A : Type} {k : ℕ} {O : PebbleRel A k} {j : Fin k} {u v : Fin k → A} (h : SetLess O j u v) (heq : MovesEq O j u v) : False

Move-set equality contradicts set comparison at the same pebble.

theorem DescriptiveComplexity.movesLess_asymm {A : Type} {k : ℕ} {O : PebbleRel A k} (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {u v : Fin k → A} (h : MovesLess O u v) : ¬MovesLess O v u

Lexicographic move-set comparison is asymmetric.

theorem DescriptiveComplexity.movesLess_trans {A : Type} {k : ℕ} {O : PebbleRel A k} (htrans : ∀ (u v w : Fin k → A), O u v → O v w → O u w) (hinc : ∀ (u v w : Fin k → A), IncompRel O u v → IncompRel O v w → IncompRel O u w) {u v w : Fin k → A} (h₁ : MovesLess O u v) (h₂ : MovesLess O v w) : MovesLess O u w

Lexicographic move-set comparison is transitive.

theorem DescriptiveComplexity.movesLess_or {A : Type} {k : ℕ} {O : PebbleRel A k} (hasymm : ∀ (u v : Fin k → A), O u v → ¬O v u) (htrans : ∀ (u v w : Fin k → A), O u v → O v w → O u w) [Finite A] {u v : Fin k → A} (h : ¬∀ (j : Fin k), MovesEq O j u v) : MovesLess O u v ∨ MovesLess O v u

If the move sets differ at some pebble, the tuples compare one way or the other lexicographically: cut at the first differing pebble.

The stage invariant

theorem DescriptiveComplexity.ordStage_invariant {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] (n : ℕ) : (∀ (u v : Fin k → A), ordStage c₀ n u v → ¬ordStage c₀ n v u) ∧ (∀ (u v w : Fin k → A), ordStage c₀ n u v → ordStage c₀ n v w → ordStage c₀ n u w) ∧ IncompRel (ordStage c₀ n) = pebbleStage (colorAgree c₀) n

The stage invariant of the ordered refinement: every stage is asymmetric and transitive, and its incomparability is the corresponding pebble stage relative to color agreement. One simultaneous induction establishes all three.

The limit

theorem DescriptiveComplexity.ordK_asymm {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] {u v : Fin k → A} (h : OrdK c₀ u v) : ¬OrdK c₀ v u

The canonical order is asymmetric.

theorem DescriptiveComplexity.ordK_trans {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] {u v w : Fin k → A} (h₁ : OrdK c₀ u v) (h₂ : OrdK c₀ v w) : OrdK c₀ u w

The canonical order is transitive.

theorem DescriptiveComplexity.incompRel_ordK_eq {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] : IncompRel (OrdK c₀) = EquivK (colorAgree c₀)

Incomparability in the canonical order is ≡ᵏ: the limit linearly orders the ≡ᵏ-classes.

theorem DescriptiveComplexity.ordK_or_of_not_equivK {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] {u v : Fin k → A} (h : ¬EquivK (colorAgree c₀) u v) : OrdK c₀ u v ∨ OrdK c₀ v u

Inequivalent tuples are comparable in the canonical order.

theorem DescriptiveComplexity.incompRel_ordK_trans {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] {u v w : Fin k → A} (h₁ : IncompRel (OrdK c₀) u v) (h₂ : IncompRel (OrdK c₀) v w) : IncompRel (OrdK c₀) u w

Incomparability in the canonical order is transitive.

theorem DescriptiveComplexity.OrdK.congr_left {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] {u v w : Fin k → A} (h : OrdK c₀ u v) (hvw : EquivK (colorAgree c₀) v w) : OrdK c₀ u w

The canonical order is a congruence for ≡ᵏ on the right.

theorem DescriptiveComplexity.OrdK.congr_right {A : Type} {k : ℕ} {β : Type u_1} [LinearOrder β] (c₀ : (Fin k → A) → β) [Finite A] {u v w : Fin k → A} (huv : EquivK (colorAgree c₀) u v) (h : OrdK c₀ v w) : OrdK c₀ u w

The canonical order is a congruence for ≡ᵏ on the left.