pairwise_insertNat
plain-language theorem explainer
Insertion of a natural number into a nondecreasing list via the hand-rolled insert keeps the list pairwise nondecreasing. Anyone proving that the Loom's sort produces a sorted certificate list cites this. The proof is induction on the list with a case split on the comparison at the head, using the insertion-permutation lemma for membership in the recursive branch.
Claim. If $l$ is a list of natural numbers that is pairwise nondecreasing under $\le$, then for every $x \in \mathbb{N}$ the list obtained by inserting $x$ into $l$ (placing $x$ before the first entry that is at least $x$, or at the end) is again pairwise nondecreasing under $\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, read up to simultaneous conjugation. The module supplies a total well-formedness checker and a computable invariant valued in traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, blind exactly to free reduction and conjugation.
As part of making the invariant deterministic, lists of natural numbers (used as sorted keys or indices in the certificate pipeline) are ordered by a hand-rolled insertion sort. The insertion function insertNat places $x$ at the first position where $x \le y$ for head $y$, otherwise recurses on the tail; the module comment stresses it is hand-rolled so no library rename can silently change the invariant.
Upstream, insertNat_perm records that the result is a permutation of $x :: l$, which is needed to transfer membership facts when the recursive branch is taken. Transitivity of $\le$ on naturals is used to chain the head comparison through already-sorted tails.
proof idea
Induction on $l$. The empty case is immediate from the definition of insertion and Pairwise on a singleton.
For $y :: t$, unpack the pairwise hypothesis into "$y$ bounds every element of $t$" and "$t$ is pairwise". Case on $x \le y$. If yes, insertion prepends $x$; the new head bounds $y$ by the case hypothesis and bounds every later element by transitivity through $y$'s bounds, while the tail stays pairwise. If no, insertion keeps $y$ and recurses; the inductive hypothesis sorts the tail, and the new head $y$ must bound the inserted $x$ (by le_of_not_le) and every other member of the inserted tail. Membership in the inserted tail is rewritten via insertNat_perm so the original pairwise bounds on $t$ apply.
why it matters
This lemma is the inductive step for pairwise_sortNat, which states that the hand-rolled sort of any list of naturals is pairwise nondecreasing. That sortedness guarantee is what lets the Loom treat sorted natural lists as canonical certificate data rather than as another quotient to manage.
In the broader Recognition setting the Loom sits downstream of the forcing chain (eight-tick octave, $D=3$) and supplies the certificate side: a finished closed-walk configuration can be checked and hashed without rebuilding it. Keeping insertion and sort internal and proved, rather than relying on Mathlib's sort API, matches the module's design rule that the invariant must not silently change under library renames. No open scaffold is involved; the result is fully proved and feeds only the sort theorem in-module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.