reduceWord_cons
plain-language theorem explainer
Free reduction of a nonempty word is head-cons reduction of the already-reduced tail: reduce(x :: t) equals consRed(x, reduce(t)). Anyone proving that SL(2,Z/3) evaluation (or any homomorphism) is blind to free reduction cites this. The proof is definitional reflexivity from the recursive clause of reduceWord.
Claim. For every integer generator label $x$ and every word $t$ (a finite list of signed cotree generators), the free reduction of the concatenated word $x{::}t$ equals the single-step reduced prepend of $x$ onto the free reduction of $t$: $\mathrm{reduce}(x{::}t)=\mathrm{consRed}(x,\mathrm{reduce}(t))$.
background
In the Loom certificate language, a closed recognition walk up to homotopy is a word in five signed cotree generators, coded as List Int. Spelling is not content: two words that freely reduce to the same reduced word represent the same loop. Free reduction is the total linear fold reduceWord, which walks the list and at each head applies consRed.
consRed x w prepends the act $x$ to an already-reduced word $w$, cancelling the head of $w$ when $x+y=0$ and otherwise leaving $x$ in front. The recursive clause of free reduction is exactly that one-step prepend on the reduced tail, so the identity proved here is the unfolding equation of the definition.
The module supplies a total well-formedness checker and a computable configuration invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ that is blind to free reduction and simultaneous conjugation; this lemma is the inductive step fuel for the reduction-invariance half.
proof idea
One-line definitional proof: rfl. By the recursive equation of reduceWord, the case x :: t is definitionally consRed x (reduceWord t), so the two sides are identical as Lean terms and no rewriting or case split is required.
why it matters
Feeds evalWord_reduceWord, which states that table evaluation of a word equals evaluation of its free reduction (under a well-formed generator table). That theorem inducts on the word, rewriting the cons case via this identity, then applying the corresponding fact for consRed and the inductive hypothesis. Without the unfolding lemma, the induction cannot align the recursive structure of evaluation with free reduction.
In the Loom story this is part of the first non-content premise: spelling is not content, so the certificate invariant must ignore free cancellation. The module header ties that blindness to closed walks on the eight-state, three-axis window (forcing-chain T7 octave, free group of rank five). The lemma itself is pure list algebra; its place in the framework is as the cheap, total bridge from raw words to reduced words that every later invariance proof uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.