insertNat_perm
plain-language theorem explainer
Insertion of a natural number into a list yields a permutation of the cons of that number onto the list. Anyone proving that the hand-rolled natural sort is a permutation of its input cites this. The argument is induction on the list with a case split on the comparison guard inside the inserter.
Claim. For every natural number $x$ and every list $\ell$ of natural numbers, the list obtained by inserting $x$ into $\ell$ (placing $x$ before the first entry that is at least $x$, or at the end if none exists) is a permutation of the list $x :: \ell$.
background
The Loom module is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. 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})$.
As part of making that invariant computable and stable, the module maintains sorted lists of naturals with a hand-rolled inserter rather than a library sort, so that no external rename can silently change the invariant. The inserter insertNat places $x$ at the head of an empty list, and on a cons cell $y::t$ returns $x::y::t$ when $x\le y$ and otherwise recurses into the tail.
The present lemma records that this structural insertion never changes multiset content: the output is always a permutation of $x$ consed onto the original list.
proof idea
Induction on the target list. The empty case is reflexivity of List.Perm. On a cons cell $y::t$, case-split on the guard $x\le y$. When the guard holds, unfolding the inserter gives $x::y::t$ on the nose, so the goal is again reflexivity. When it fails, unfolding gives $y$ consed onto the recursive insertion; the inductive hypothesis supplies a permutation of the tails, consing $y$ preserves it, and a single adjacent swap of $x$ past $y$ finishes the chain to $x::y::t$.
why it matters
This is the permutation half of the correctness of the hand-rolled natural sort used inside Loom's certificate machinery. Downstream, sortNat_perm is proved by induction exactly by composing this lemma with cons-preservation of permutations, so every sorted list is a permutation of its input. The companion pairwise_insertNat shows the inserter preserves the pairwise $\le$ predicate, so together the two lemmas certify that sorting is a stable content-preserving normalisation rather than a content-changing rewrite.
In the Loom setting that matters because the invariant must be blind only to free reduction and simultaneous conjugation, never to accidental reordering of auxiliary numeric data. Keeping the sort local and proved here keeps the certificate checker trustworthy on finished objects it did not build. The result is pure list combinatorics; it does not itself touch the free-group or $\mathrm{SL}(2,\mathbb{Z}/3)$ layers, but those layers depend on it for normalisation hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.