≡ᵏ 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.relsIn_blockRelsExtend_univ {L : FirstOrder.Language} {B : SOBlock} {α : Type u_1} {n : ℕ} (φ : (L.sum B.lang).BoundedFormula α n) : RelsIn (blockRelsExtend Set.univ B) φ

Over the full agreement family there is nothing to check: every formula's relation symbols lie in it.

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

theorem DescriptiveComplexity.exists_notMem_image_erase {A : Type} {k : ℕ} [Finite A] (w : Fin k → A) (i : Fin k) (hA : k ≤ Nat.card A) : ∃ (d : A), ∀ (j : Fin k), j ≠ i → w j ≠ d

A tuple of k elements leaves a k-element set an element to spare once one of its pebbles is freed.

theorem DescriptiveComplexity.update_pattern {A : Type} {k : ℕ} {B : Type} {v : Fin k → A} {w : Fin k → B} {c : A} {d : B} (hpat : ∀ (p q : Fin k), v p = v q ↔ w p = w q) (i : Fin k) (hc : ∀ (j : Fin k), j ≠ i → (v j = c ↔ w j = d)) (p q : Fin k) : Function.update v i c p = Function.update v i c q ↔ Function.update w i d p = Function.update w i d q

Replacing a pebble on both sides by a matching pair of elements – matching in the sense that each other coordinate hits the new element on the left exactly when it does on the right – preserves the equality pattern.

theorem DescriptiveComplexity.exists_update_pattern {A : Type} {k : ℕ} [Finite A] (hA : k ≤ Nat.card A) {v w : Fin k → A} (hpat : ∀ (p q : Fin k), v p = v q ↔ w p = w q) (i : Fin k) (c : A) : ∃ (d : A), ∀ (p q : Fin k), Function.update v i c p = Function.update v i c q ↔ Function.update w i d p = Function.update w i d q

The duplicator's answer on a bare set: whichever pebble is moved wherever, the equality pattern can be restored – by the matching repetition, or by a fresh element, of which there is one since the moved pebble no longer constrains the answer.

≡ᵏ 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.inflLimit_swap_bare {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) (x y : A) : (d.inflLimit A i fun (p : Fin (d.B.arity i)) => ![x, y] (Fin.cast harity p)) ↔ d.inflLimit A i fun (p : Fin (d.B.arity i)) => ![y, x] (Fin.cast harity p)

A binary variable of an order-free induction is symmetric on a bare set: the transposition exchanging the two arguments leaves the equality pattern of the tuple alone, so ≡ᵏ-invariance (DescriptiveComplexity.StepDef.inflLimit_invariant) cannot tell the pair from the swapped pair.

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.