consRed
plain-language theorem explainer
Prepends one signed generator to a freely reduced word, cancelling the head pair when the new letter is the inverse of the current head. Free reduction and the matrix-evaluation lemmas that show reduction preserves the SL(2, Z/3Z) word map both call this step. The body is a single pattern match on the target list: empty, cancel, or cons.
Claim. For an integer letter $x$ and a word $w$ (a finite list of integers coding signed cotree generators), the reduced prepend is: if $w=\emptyset$ then $[x]$; if $w=y::r$ and $x+y=0$ then $r$; otherwise $x::y::r$.
background
Loom treats a finished recognition history as a finite list of closed walks on the eight-state, three-axis window. Up to homotopy those walks form a free group of rank five, so each loop is a word in five signed generators. Content is read only up to free reduction (spelling is not content) and up to simultaneous conjugation (basepoint is not content).
A Word is simply a list of integers. Free reduction must be total and linear so every well-formedness check stays cheap. The one-step primitive is this reduced prepend: given an already reduced tail, attach a new letter and cancel only if it is the inverse of the current head. Full free reduction is then the fold of that step from the right.
The module later evaluates reduced words in SL(2, Z/3Z) and reads traces of loops and pairwise commutators; those maps must ignore free cancellation, which is why the one-step identity for evaluation under reduced prepend is proved separately.
proof idea
Definition by cases on the target word, not a theorem. Empty list becomes the singleton [x]. Nonempty head y :: r branches on whether x + y = 0: if so the head pair cancels and the result is the remainder r; otherwise the letter is consed, yielding x :: y :: r. No lemmas are invoked.
why it matters
This is the atomic step of free reduction in the Loom certificate language. reduceWord is defined as folding it over the input, and reduceWord_cons is the corresponding one-line unfold. Preservation of the reduced predicate (isReduced_consRed) and compatibility with matrix evaluation (evalWord_consRed: the SL(2, Z/3Z) image multiplies by the letter matrix) both case-split on the same cancel/cons branch.
In the framework this implements the first non-content premise from the module header: spelling is not content, so closed walks are identified up to free reduction in the rank-five free group forced by the eight-tick window (T7) and D = 3 (T8). Without a total linear cancel step, the checker and the trace invariant would not be computable on finished utterances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.