reduceWord
plain-language theorem explainer
Free reduction of a word in the five signed cotree generators: reduce the tail, then prepend the head via adjacent cancellation. Loom users cite it as the total linear normalizer that makes every well-formedness check cheap and decidable. Defined by structural recursion through the one-letter prepend-with-cancel step.
Claim. For a word $w$ (a finite list of integers, read as a closed walk in the free group on five signed cotree generators), the free reduction of $w$ is: empty on the empty word; on $x{::}t$, prepend $x$ to the free reduction of $t$ with cancellation whenever the new head and the next letter sum to zero.
background
Loom is a certificate language for finished 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 $E-V+1=5$. A word is therefore a finite list of integers (signed cotree generators), and an utterance is a finite list of such words sharing one basepoint.
Spelling is not content: two words that differ only by free cancellation represent the same loop. The one-letter step consRed prepends a generator to an already reduced word and drops the pair when head and next letter sum to zero. Free reduction is the fold of that step over the whole list.
The module supplies a total checker, a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3)$, and theorems that the invariant is blind to free reduction and simultaneous conjugation. No model or search is carried.
proof idea
Pure structural recursion on the list, not a proved theorem. The empty word maps to itself. A cons cell reduces the tail first, then applies the one-letter prepend-with-cancel step to the head and that reduced tail. The companion equation reduceWord (x :: t) = consRed x (reduceWord t) is definitional (rfl).
why it matters
This is the normalizer every Loom certificate runs through. Downstream, isReduced_reduceWord shows the checker really accepts the output ("reduction really reduces"); evalWord_reduceWord shows the $\mathrm{SL}(2,\mathbb{Z}/3)$ evaluation is invariant under it; reduceConfig maps it over whole utterances; conjWord builds basepoint moves as reduce of $g,w,g^{-1}$; and weaveBody reduces each production so grammar output is already reduced. Together these discharge the module claim that spelling is not content, so the invariant can be trusted on finished objects it did not build. Lands in the free-group layer of the eight-tick window (T7), not in the J-cost or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.