pairwise_sortNat
plain-language theorem explainer
Insertion-sorting a list of naturals yields a pairwise non-decreasing list. Anyone proving that the hand-rolled sort is a canonical representative of a permutation class cites this. The proof is a short induction whose inductive step is the companion insert-preserves-sortedness lemma.
Claim. For every finite list $\ell$ of natural numbers, the list obtained by insertion-sorting $\ell$ is pairwise non-decreasing: consecutive (and hence all) entries satisfy $\le$.
background
The Loom module is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window. Configurations are finite lists of freely reduced words in five signed generators; the computable invariant reads SL(2, Z/3Z) traces of the loops and of their pairwise commutators. Those commutator traces are collected over ordered index pairs, so the module needs a stable ordering of natural indices that cannot silently change under library renames.
sortNat is therefore a hand-rolled insertion sort: the empty list sorts to empty, and a cons cell inserts its head into the already-sorted tail via insertNat. Mathlib's List.Pairwise (· ≤ ·) is the standard inductive predicate that every earlier element is ≤ every later one.
The immediate upstream fact is pairwise_insertNat: if a list is already pairwise ≤, inserting one more natural preserves that property. That lemma is itself proved by induction on the target list.
proof idea
Term-mode induction on the input list. The nil case is List.Pairwise.nil. The cons case applies pairwise_insertNat to the head and the already-sorted tail, feeding the inductive hypothesis that the sorted tail is pairwise ≤. No extra arithmetic or rewriting is required.
why it matters
This is the sortedness half of the uniqueness argument for the hand-rolled sort. The sole downstream consumer is sortNat_eq_of_perm: if two lists are permutations of each other, their sortNat images coincide, proved by Mathlib's List.Perm.eq_of_pairwise' once both images are known pairwise ≤ and both are permutations of the inputs.
In the Loom invariant, commutator traces are emitted over index pairs in a fixed order. Equality of sorted index lists under permutation therefore guarantees that reordering the loops of a configuration does not change the invariant payload. That blindness is part of the module's charter: the invariant must ignore exactly the two non-content operations (free reduction and simultaneous conjugation), and stable ordering of auxiliary indices is infrastructure for the commutator half of the reading. No forcing-chain landmark (T5–T8, RCL, φ) is touched directly; this is pure list infrastructure inside the certificate layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.