sortLex
plain-language theorem explainer
Lexicographic insertion sort on lists of integer vectors. It turns an unordered collection of abelianised loop exponents into a unique sorted list, so two configurations that differ only by loop order compare equal. Cited by the depth-one abelian reading of a Loom utterance. The body is ordinary recursive insertion via the companion insert step.
Claim. Define a total map $\mathrm{sort}_{\mathrm{lex}} : \mathrm{List}(\mathrm{List}\,\mathbb{Z}) \to \mathrm{List}(\mathrm{List}\,\mathbb{Z})$ by $\mathrm{sort}_{\mathrm{lex}}([]) = []$ and $\mathrm{sort}_{\mathrm{lex}}(v :: t) = \mathrm{insert}_{\mathrm{lex}}(v,\,\mathrm{sort}_{\mathrm{lex}}(t))$, where $\mathrm{insert}_{\mathrm{lex}}$ places a vector into an already sorted list under lexicographic order on $\mathbb{Z}$-lists.
background
Loom treats a finished recognition utterance as a finite list of reduced words in the free group of rank five (the closed-walk fundamental group on the eight-state, three-axis window). Content is blind to free reduction and to simultaneous conjugation; the module supplies a computable invariant with exactly those two blindnesses.
Abelianisation sends each loop word to its exponent vector in $\mathbb{Z}^5$. The resulting list of vectors is only a multiset: order of loops is not content. To obtain a canonical representative one must sort those vectors. Lexicographic order on List Int is the comparison used here; the companion insertLex inserts one vector into an already sorted list by that order.
The surrounding invariant also reads depth-two commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3)$, because pure loop traces collide on some automorphism images. The sorted abelian list is only the depth-one layer of that reading.
proof idea
Definition by structural recursion on the outer list: empty list sorts to empty; a cons cell inserts the head into the recursively sorted tail. Insertion is delegated entirely to insertLex, which walks the sorted spine and places the new vector at the first position where lexicographic $\le$ holds. No lemmas are invoked; the definition is the algorithm.
why it matters
Feeds abelBag, the depth-one reading of a Loom configuration: map each loop through abelianisation, then sort the resulting exponent lists. Without a canonical order, the abelian multiset would depend on presentation order and could not sit inside a conjugation- and permutation-blind certificate.
In the module's division of labour, this is pure scaffolding for the invariant: well-formedness checking and the two blindness theorems (invariantOf_perm, invariant_conjWord and kin) rely on every intermediate reading being a pure function of content. Sorting under lex order is the cheapest total normal form for the abelian layer.
It does not itself touch the forcing chain (T0–T8), the J-cost, or the eight-tick octave; it only normalises data those structures produce when closed walks are read as free-group words.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.