evalWord_consRed
plain-language theorem explainer
Matrix evaluation of a free-reduction prepend equals the letter matrix times the evaluation of the tail. Anyone showing that free reduction preserves the SL(2, Z/3Z) word map cites this lemma. The proof cases on empty versus nonempty tail and on whether the new letter cancels the head.
Claim. Let $T$ be a well-formed generator table, $x\in\mathbb{Z}$ a signed letter, and $u$ a word in the five cotree generators. Writing $\mathrm{consRed}(x,u)$ for the free-reduction prepend of $x$ onto $u$, one has $\mathrm{eval}(T,\mathrm{consRed}(x,u))=L_T(x)\,\mathrm{eval}(T,u)$, where $L_T(x)$ is the matrix assigned to letter $x$.
background
Loom treats finished recognition histories as finite lists of closed walks on the eight-state, three-axis window. Up to homotopy those walks are words in five signed generators (free group of rank $E-V+1=5$). Spelling is not content, so words are identified up to free reduction: consecutive inverse letters cancel.
A Table assigns to each generator a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ (the image and the inverse image). Word evaluation multiplies those letter matrices left-to-right; the empty word is the identity. Free-reduction prepend either cancels the head letter when $x+y=0$, or else ordinary cons.
The module supplies a total well-formedness checker and a computable configuration invariant (loop traces plus pairwise commutator traces) that must be blind to free reduction and to simultaneous conjugation. This lemma is the local multiplicative step that makes reduction-invariance of evaluation hold.
proof idea
Case on the tail $u$.
If $u$ is empty, free-reduction prepend is a singleton; rewrite by the singleton evaluation rule and right-multiply by one.
If $u=y::r$, split on whether $x+y=0$. On cancellation, $y=-x$; free-reduction prepend drops both letters, so the claim becomes $L_T(x)L_T(-x),\mathrm{eval}(T,r)=\mathrm{eval}(T,r)$. Associativity plus the table axiom that inverse letters multiply to the identity, then left-multiply by one, finishes. On non-cancellation, free-reduction prepend is ordinary cons, and the ordinary cons-evaluation rule applies directly.
why it matters
The sole downstream consumer is the induction step of evaluation-invariance under full free reduction: reducing a cons rewrites through free-reduction prepend, applies this lemma, then the inductive hypothesis and ordinary cons-evaluation. That theorem is exactly the algebraic half of "spelling is not content" in the Loom header: the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ word map (and therefore the trace-and-commutator invariant built from it) cannot see free reduction.
In the broader Recognition picture this sits on the eight-tick, three-axis window forced by T7–T8. Closed walks form the free group of rank five; the Loom certificate language quotients by the two non-content operations (reduction and basepoint conjugation) and reads a class-function invariant. Without this multiplicative compatibility, the invariant would depend on spelling rather than on the reduced conjugacy data the framework treats as meaning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.