≡ᵏ on a bare set, and the order an induction cannot define

The invariant layer, read over the empty vocabulary. There ≡ᵏ collapses as far as it can: two k-tuples are equivalent as soon as they satisfy the same equalities between coordinates (DescriptiveComplexity.equivK_bare), provided the set has k elements to spare – the duplicator answers a repeated pebble by the matching repetition and a fresh one by a fresh one, and only k - 1 pebbles constrain the answer since the moved one is being replaced.

The consequence is the theorem this file exists for (DescriptiveComplexity.not_isLinearOrder_inflLimit): no order-free inflationary induction defines a linear order on a bare set. Every stage of such an induction is ≡ᵏ-invariant (DescriptiveComplexity.StepDef.inflLimit_invariant), and a transposition of the universe carries any pair to the swapped pair without changing the equality pattern, so a binary variable of the limit is symmetric – which no antisymmetric total relation on two distinct points can be.

This is what turns the order-invariant convention of this library into a theorem: the linear order that DescriptiveComplexity.IFPDefinable, DescriptiveComplexity.TCDefinable and the rest are handed is not a convenience, it is something no isomorphism-invariant logic can produce for itself.

What it is not is a statement about a complexity class. It concerns a defined relation; a Boolean query is separated by comparing two structures of different sizes, which nothing in this layer does – ≡ᵏ relates tuples inside one structure. The class-level statement (order-free FO(IFP) does not capture PTIME, at DescriptiveComplexity.EVEN) needs the two-structure pebble game and is a separate development.

Every induction reads every symbol

theorem DescriptiveComplexity.StepDef.usesRels_univ {L : FirstOrder.Language} (d : StepDef L) : d.UsesRels Set.univ

Every induction uses symbols of the full family: the hypothesis of the invariance theorems is free when one does not care which symbols are read.

Moving a pebble on a bare set

≡ᵏ over the empty vocabulary

theorem DescriptiveComplexity.equivK_bare {A : Type} {k : ℕ} [FirstOrder.Language.empty.Structure A] [Finite A] {S : Set ((n : ℕ) × FirstOrder.Language.empty.Relations n)} (hA : k ≤ Nat.card A) {v w : Fin k → A} (hpat : ∀ (p q : Fin k), v p = v q ↔ w p = w q) : EquivK (atomicAgreeOn S A k) v w

On a bare set, ≡ᵏ is the equality pattern: two k-tuples over the empty vocabulary satisfying the same equalities between coordinates are ≡ᵏ-equivalent, as soon as the set has k elements. The strategy is DescriptiveComplexity.exists_update_pattern, fed to the coinduction principle DescriptiveComplexity.le_equivK.

The order no order-free induction defines

theorem DescriptiveComplexity.not_isLinearOrder_inflLimit {k : ℕ} (d : StepDef FirstOrder.Language.empty) {i : d.B.ι} (hd : d.VarBound k) (harity : d.B.arity i = 2) (A : Type) [FirstOrder.Language.empty.Structure A] [Finite A] (hA : k ≤ Nat.card A) : ¬IsLinearOrder A fun (x y : A) => d.inflLimit A i fun (p : Fin (d.B.arity i)) => ![x, y] (Fin.cast harity p)

No order-free inflationary induction defines a linear order on a bare set. On a set with at least k elements – k a variable budget of the induction – every binary variable of the limit is symmetric (DescriptiveComplexity.inflLimit_swap_bare), and a symmetric relation on two distinct points is not both antisymmetric and total. The two distinct points are there because a binary variable forces 2 ≤ k ≤ Nat.card A.

This is the order-invariance of the library's definability notions, as a theorem: what a first-order induction is handed with the order, it cannot build. Registered in the Lax archive as Lax945089.NoDefinableOrder.not_isLinearOrder_inflLimit.