sortNat_perm
plain-language theorem explainer
Hand-rolled insertion sort of a finite list of naturals is always a permutation of that list. Cited wherever Loom needs the sorted index list to be multiset-faithful before comparing invariants. Proof is list induction, composing the insertion-permutation lemma with the inductive hypothesis and cons-congruence of Perm.
Claim. For every finite list $\ell$ of natural numbers, the hand-rolled insertion sort of $\ell$ is a list-permutation of $\ell$.
background
Loom 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; the module supplies a total well-formedness checker and a computable invariant valued in traces in $SL(2,\mathbb{Z}/3\mathbb{Z})$, including traces of pairwise commutators.
The hand-rolled sortNat is ordinary insertion sort on List Nat, defined by inserting the head into the recursively sorted tail via insertNat. It is kept local so that no library rename can silently change what the invariant reads. The companion lemma insertNat_perm states that inserting $x$ into a list yields a permutation of $x$ cons that list.
Permutation reasoning appears because both sides of later equality theorems build sorted index lists in the same order; once sorting is known to be a permutation, equality of sorted outputs follows from pairwise-sorted uniqueness.
proof idea
Term-mode induction on the input list. The empty case is reflexivity of List.Perm. In the cons case, the inductive hypothesis says the sorted tail is a permutation of the tail; insertNat_perm says inserting the head into the sorted tail is a permutation of head cons sorted-tail; transitivity with cons-congruence of Perm closes the step.
why it matters
Feeds sortNat_eq_of_perm, which concludes that permutation-equivalent lists have identical sortNat images, via pairwise-sorted uniqueness and the two applications of this lemma. That equality is what lets the Loom invariant treat sorted index data as a multiset canonical form when comparing traces of pairwise commutators across configurations. Without multiset fidelity of the sort, the depth-two lower-central-series reading would depend on presentation order rather than on the conjugacy-blind content the module isolates. The result is pure list combinatorics inside Loom.Core; it does not itself touch the forcing chain, but it underwrites the certificate side of closed recognition walks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.