evalWord_cons
plain-language theorem explainer
Prepending a signed generator letter to a word multiplies the word's matrix image on the left by that letter's matrix. Anyone proving free-reduction, inversion, or substitution invariance of the Loom evaluation cites this. The proof is pure definitional equality (rfl) against the structural clause of evalWord.
Claim. For any generator table $T$, integer letter $x$, and word $t$, the matrix image of the cons word $x{::}t$ equals the product of the letter matrix of $x$ with the matrix image of $t$: $\mathrm{eval}(T,x{::}t)=\mathrm{letter}(T,x)\,\mathrm{eval}(T,t)$.
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 are words in five signed cotree generators, written as lists of integers (Word). A Table assigns to each generator a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$: the image of the generator and the image of its inverse.
Evaluation of a word is the monoid homomorphism that sends the empty word to the identity and multiplies letter matrices left-to-right. The single-letter map picks the forward or inverse matrix according to the sign of the integer (and the identity for zero). The module's invariant is built from traces of these images and of their pairwise commutators, so every later blindness theorem needs a clean recursive law for evaluation.
The definition of evaluation is deliberately structural on the head, so the cons case is definitional rather than a separate lemma that must be proved by induction.
proof idea
One-line wrapper: rfl. Unfolding evalWord on a cons cell yields exactly letterMat T x * evalWord T t by the second clause of the definition, so the equality is definitional.
why it matters
This is the recursive engine under every evaluation-preservation theorem in Loom.Core. Free reduction (evalWord_consRed, then evalWord_reduceWord) rewrites a reduced cons and needs the plain cons law to match the unreduced side. Inversion (evalWord_invWord) inducts on the word and multiplies through the cons clause. Substitution under window automorphisms (evalWord_substWord) likewise inducts by cons, then reassociates via this identity; its doc-comment notes that this is what lets the forty-eight automorphisms be checked by changing the table rather than rewriting every word.
In the broader Recognition picture the Loom invariant certifies closed walks on the eight-tick window forced by T7, reading them in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Without a definitional cons law the free-group and conjugation-blindness arguments would carry an extra inductive obligation at every step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.