insertLex
plain-language theorem explainer
Lexicographic insertion of one integer list into a list of integer lists: place the new word at the first position where it is not strictly after the head under dictionary order. The Loom sort that canonicalises the multiset of abelianised loops is built by folding this insertion. The body is plain structural recursion on the target list, branching on the Boolean comparator leLexInt.
Claim. Define insertion of a word $v \in \mathbb{Z}^*$ into a list $L$ of words by: if $L$ is empty, return $[v]$; if $L = u :: t$, return $v :: u :: t$ when $v \le_{\mathrm{lex}} u$, otherwise $u ::$ (insert $v$ into $t$). Here $\le_{\mathrm{lex}}$ is the standard lexicographic order on integer lists (empty prefix is smallest; first differing entry decides).
background
Loom treats a finished recognition utterance as a finite list of reduced words in five signed generators (the free group of rank $E-V+1=5$ on the eight-state, three-axis window). Spelling and basepoint are not content, so configurations are read up to free reduction and simultaneous conjugation. The module supplies a total well-formedness checker and a computable invariant blind to those two operations.
Integer lists here are the abelianised images of those loops (generator exponents). The comparator leLexInt is ordinary dictionary order on List Int: empty is least; at the first differing coordinate the smaller integer wins; equal heads recurse on the tails.
insertLex is the classical insertion step used to keep a list of such words sorted under that order. It assumes nothing about freeness or reduction; it is pure list combinatorics sitting under the depth-one reading of an utterance.
proof idea
Definition by recursion on the target list, not a theorem. Base case: insert into [] yields the singleton. Inductive case: compare the new word to the head via leLexInt; if already less-or-equal, cons in front, else keep the head and recurse on the tail. No lemmas are invoked; the Boolean branch is the entire control flow.
why it matters
Immediate consumer is sortLex, which folds insertLex over a list of words and is documented as the depth-one reading of an utterance: the multiset of abelianised loops. That multiset is the first layer of the Loom invariant; the full invariant also records traces of pairwise commutators in $\mathrm{SL}(2,\mathbb{Z}/3)$ so that conjugation-blind class functions separate configurations the abelianisation alone collides.
Without a stable sort of the abelianised words, the multiset would depend on presentation order and could not serve as a certificate. This helper is the mechanical piece that makes the depth-one layer order-independent. It sits inside the certificate language for closed recognition walks on the eight-tick window forced by T7, not inside the forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.