leLexInt
plain-language theorem explainer
Boolean lexicographic comparison on lists of integers: empty is least, heads decide, equal heads recurse on tails. The Loom certificate layer uses it to keep integer vectors sorted when building a canonical multiset of reduced words. Pure structural recursion on the two lists; no lemmas required.
Claim. Define a Boolean relation $\mathrm{le}_{\mathrm{lex}}$ on $\mathrm{List}\,\mathbb{Z}$ by: $\mathrm{le}_{\mathrm{lex}}([],\,ys)=\mathrm{true}$ for every $ys$; $\mathrm{le}_{\mathrm{lex}}(x{::}xs,\,[])=\mathrm{false}$; and $\mathrm{le}_{\mathrm{lex}}(x{::}xs,\,y{::}ys)$ is $\mathrm{true}$ if $x<y$, $\mathrm{false}$ if $y<x$, and $\mathrm{le}_{\mathrm{lex}}(xs,ys)$ if $x=y$.
background
Loom is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. Closed walks up to homotopy form a free group of rank five, so a finished utterance is a finite list of words in five signed generators sharing one basepoint. Content is read up to free reduction and up to simultaneous conjugation (basepoint change); the module supplies a total well-formedness checker and a computable invariant blind to those two operations.
Integer lists appear as the raw spelling of reduced words (and related vectors) before they are fed to the invariant, which reads traces and pairwise commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Ordering those vectors lexicographically is the bookkeeping step that turns an unordered collection into a sorted list so the invariant can be evaluated deterministically.
proof idea
Definition by nested pattern match, not a proved theorem. Three clauses: empty left argument yields true; nonempty left and empty right yields false; both nonempty compare heads with the integer order and, on equality, recurse on the tails. Termination is immediate from list length.
why it matters
Sole consumer in-module is insertLex, the insertion step that places a fresh integer vector into an already lexicographically sorted list of vectors. That sorted list is the canonical representative of a multiset of reduced words (or related integer data) before the Loom invariant is computed. Without a total Boolean order, the certificate layer could not normalize configurations independently of presentation order. The comparison itself is ordinary discrete math; its place in the framework is purely infrastructural support for the conjugation-blind, reduction-blind certificate checker described in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.