evalWord
plain-language theorem explainer
Evaluation sends a free-group word in the five signed cotree generators to a left-to-right product of matrices in Mat_2(Z/3Z) drawn from a generator table. Anyone proving the Loom invariant is blind to free reduction or simultaneous conjugation cites this map. Defined by structural recursion on the letter list: empty word to identity, cons multiplies the letter matrix on the left.
Claim. Fix a generator table $T$ assigning to each of five generators a pair of matrices in $\mathrm{Mat}_2(\mathbb{Z}/3\mathbb{Z})$ (image and inverse image). The evaluation of a word $w=(x_1,\ldots,x_n)\in\mathbb{Z}^*$ is the product $\ell_T(x_1)\cdots\ell_T(x_n)$, where $\ell_T(x)$ is the matrix for generator $|x|$ or its inverse according to the sign of $x$, and the empty word evaluates to the identity.
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window forced by the T0–T8 chain. Closed walks up to homotopy form a free group of rank five, so a finished utterance is a finite list of words in five signed generators sharing one basepoint.
A word is a List Int (positive index for a generator, negative for its inverse). Matrices are stored by components over ZMod 3 rather than as Matrix, so thousands of products reduce cheaply in the kernel. A table is a list of pairs (M, M^{-1}), one pair per generator; letterMat looks up the signed letter in that table (zero maps to the identity).
The module supplies a total well-formedness checker, a computable invariant valued in traces and commutator traces in SL(2, Z/3Z), and theorems that the invariant is blind exactly to free reduction and simultaneous conjugation. Evaluation of words is the first step of that invariant.
proof idea
Pure structural recursion on the list: the empty word maps to the multiplicative identity of Mat; a cons cell multiplies letterMat T x on the left by the recursive evaluation of the tail. No tactics, no lemmas. The head-structural shape is what makes the later append homomorphism a one-line induction.
why it matters
This is the representation homomorphism from free words into the matrix monoid that every Loom certificate reads. Downstream, det_evalWord shows the image lands in SL(2, Z/3Z) when the table is well-formed; evalConfig lifts evaluation to whole utterances; evalWord_append makes it a monoid homomorphism; evalWord_invWord, evalWord_reduceWord, and evalWord_conjWord prove blindness to free reduction and basepoint change (conjugation), which is the content of the two non-content premises in the module header.
Those blindness theorems are why trace (a class function) and pairwise commutator traces can serve as the invariant: spelling and starting vertex are not content. The construction sits on the free group of rank five coming from the eight-tick octave and D=3 window; it carries no model and no search, only the evaluation map a finished certificate is checked against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.