insertNat
plain-language theorem explainer
Insertion of a natural number into a list, placing it before the first entry that is at least as large (or at the end). Used inside the Loom hand-rolled sort so the configuration invariant is a sorted multiset of traces, not an order-dependent list. Defined by a single recursive case split on the head.
Claim. Define a map that sends a natural number $x$ and a list $\ell$ of naturals to a new list: on the empty list return $[x]$; on $y{::}t$, if $x \le y$ prepend $x$ to $y{::}t$, otherwise keep $y$ and recurse into $t$.
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to free reduction and simultaneous conjugation become words in a free group of rank five; a configuration is a finite list of such words at one basepoint. The module supplies a total well-formedness checker and a computable invariant, with no model or search.
The invariant evaluates loops in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and records ordinary traces together with traces of pairwise commutators (depth-two lower-central data). Trace is a class function, so conjugation blindness is algebraic. Because the invariant must read a multiset rather than a list order, the module sorts those natural-number traces with a local insertion routine instead of a library sort, so a rename cannot silently change the meaning of the invariant.
proof idea
Pure definition by structural recursion on the list: empty case returns the singleton; cons case compares $x$ with the head and either conses $x$ in front or keeps the head and recurses. No lemmas are applied; the body is the algorithm.
why it matters
Feeds the hand-rolled sortNat fold and the two supporting facts that insertion is a permutation of cons and that it preserves pairwise nondecreasing order. Those facts make the sorted trace lists honest multisets, which is required for the Loom invariant to be blind exactly to free reduction and simultaneous conjugation and nothing else. Sits in the certificate layer of the recognition-walk story (closed histories on the eight-tick window, free group of rank five), not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.