isReduced_consRed
plain-language theorem explainer
Prepending a signed generator to a freely reduced word, with immediate free cancellation when the head is its inverse, again yields a freely reduced word. Anyone proving that free reduction is total and correct cites this lemma. The argument is a short case split on the empty word versus a nonempty head, then on whether the new letter cancels.
Claim. Let $u$ be a word in the five signed cotree generators that is already freely reduced, and let $x\in\mathbb{Z}$ be a generator label. Form the word obtained by prepending $x$ to $u$ and cancelling the head pair if $x$ is the inverse of the first letter of $u$. That resulting word is freely reduced.
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 integer generator labels, and spelling is not content: words are identified up to free reduction.
consRed is the one-step reduced prepend: given a letter $x$ and an already reduced word, it returns $[x]$ on the empty word, drops the head if $x$ cancels it ($x+y=0$), and otherwise conses $x$ in front. Free reduction of a whole word is the left fold of this operation. The boolean predicate isReduced checks that no consecutive inverse pair remains.
The local setting is purely syntactic. The module supplies a total checker, a computable $SL(2,\mathbb{Z}/3)$ trace invariant (including pairwise commutator traces), and theorems that the invariant is blind to free reduction and simultaneous conjugation. No model or search is involved.
proof idea
Case on the already-reduced word $u$.
If $u$ is empty, consRed returns the singleton $[x]$, which is reduced by definition (rfl).
If $u = y::r$, split on whether $x+y=0$. On cancellation, consRed returns the tail $r$; isReduced_tail applied to the hypothesis that $u$ is reduced gives that $r$ is reduced. On non-cancellation, consRed returns $x::y::r$; rewrite with isReduced_cons_cons and discharge the two conjuncts of the boolean and: the head pair is non-inverse (from the case hypothesis via bne_iff_ne), and the remainder $y::r$ is already reduced by assumption.
why it matters
This is the inductive step that makes free reduction honest. The sole downstream consumer is isReduced_reduceWord, whose doc-comment states the checker's specification: "reduction really reduces. Without this the checker's verdict would be a wish rather than a fact." That theorem is proved by induction on the word, applying exactly this lemma at the cons step.
In the broader Loom story, a finished utterance is a finite list of freely reduced words sharing a basepoint, and content is what survives free reduction and simultaneous conjugation. The eight-tick octave and $D=3$ fix the window whose cotree has five signed generators; free reduction is the first of the two non-content operations the certificate language must quotient by. Closing the reducedness invariant is what lets the total checker be trusted on objects it did not build.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.