sortNat
plain-language theorem explainer
Hand-rolled insertion sort on lists of naturals, used to canonicalize multisets of loop traces and pairwise-commutator traces in the Loom configuration invariant. Anyone citing invariantOf or its permutation-invariance lemmas depends on this. Defined by recursion on the list: empty stays empty; a cons inserts the head into the already-sorted tail via insertNat.
Claim. Define $\mathrm{sort}:\mathrm{List}\,\mathbb{N}\to\mathrm{List}\,\mathbb{N}$ by $\mathrm{sort}([])=[]$ and $\mathrm{sort}(x::t)=\mathrm{insert}(x,\mathrm{sort}(t))$, where $\mathrm{insert}$ places a natural into a sorted list while preserving nondecreasing order.
background
Loom is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window from the forcing chain. Closed walks up to homotopy form a free group of rank five; a finished utterance is a finite list of such words sharing a basepoint. Content is read up to free reduction and simultaneous conjugation, so the module supplies a computable invariant blind to those two non-content operations.
The invariant maps each loop image in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ to its trace, and also records traces of pairwise commutators (depth-two lower-central-series data). Both components are lists of naturals. Sorting those lists turns them into order-independent canonical representatives of multisets, so the invariant does not depend on the order in which loops were listed.
The definition is deliberately local rather than Mathlib's sort, so a library rename cannot silently change what the invariant computes.
proof idea
Pure recursive definition, not a theorem. The empty list maps to itself. On a cons cell $x::t$, recursively sort the tail and insert $x$ into that sorted list with the companion inserter insertNat. No tactics or lemmas are applied at the definition site; correctness (permutation, pairwise orderedness, equality under permutation) is proved downstream.
why it matters
This is the canonicalization step inside invariantOf, which returns the pair (sorted loop traces, sorted pairwise-commutator traces). Depth one is what an amplitude-style reading can see; depth two is what abelianization destroys. Downstream lemmas sortNat_perm, pairwise_sortNat, and sortNat_eq_of_perm establish that the output is a sorted permutation of the input and is constant on permutation classes, which is exactly what makes the Loom invariant well-defined on configurations rather than on particular list presentations.
In the broader Recognition setting the Loom module certifies finished closed histories on the eight-tick window without carrying a model or a search. Stable, hand-owned sorting keeps that certificate language independent of Mathlib churn.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.