det_evalWord
plain-language theorem explainer
Any word evaluated under a well-formed generator table lands in SL(2, Z/3Z): its matrix has determinant one. Loom invariant proofs cite this whenever conjugation or substitution must preserve the SL condition. The argument is induction on the word, using that each letter matrix already has det 1 and det is multiplicative.
Claim. Let $T$ be a well-formed table assigning to each signed generator a pair of $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$. For every finite word $w$ in those generators, if $M_T(w)$ is the product of the corresponding letter matrices, then $\det M_T(w)=1$.
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to homotopy are words in five signed cotree generators; an utterance is a finite list of such words sharing a basepoint. Content is quotiented by free reduction and by simultaneous conjugation (basepoint move).
Matrices here are explicit $2\times 2$ blocks over $\mathbb{Z}/3\mathbb{Z}$ (four components $a,b,c,d$), chosen so thousands of products reduce in the kernel. A table lists, for each generator, the image matrix and the image of its inverse. Evaluating a word multiplies those letter matrices in order; the empty word is the identity.
The module invariant reads traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and traces of pairwise commutators. Membership in $\mathrm{SL}$ is exactly determinant one, so every evaluated word must stay in that group if the table is well-formed.
proof idea
Induct on the word. For the empty word, evaluation is the identity matrix and $\det I=1$ (via Mat.det_one).
For a cons cell, evaluation is the product of the head letter matrix with the evaluation of the tail. Multiplicativity of determinant, the inductive hypothesis that the tail has det 1, and the letter lemma that every well-formed table sends each signed generator to a matrix of det 1, reduce the product of determinants to $1\cdot 1=1$.
why it matters
This is the SL-membership lemma for the Loom representation. Downstream, conjugation blindness at depth one (trN_conjWord) rewrites the conjugated evaluation and applies the class-function identity for trace, which needs $\det=1$ on the conjugating matrix. The bundled soundness fact invariant_conjWord (respelling and shared basepoint move leave the invariant fixed) rests on the same evaluation-conjugation identity. Table substitution soundness (ok_tableOfSubst) re-checks well-formedness after replacing generators by words, and quotes this theorem to keep det 1 on the new images.
In the framework, the free group of rank $E-V+1=5$ on the eight-tick window is read through $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ so that conjugation is a ring identity rather than a canonicalisation. Without det 1 on every word, the adjugate would not serve as the inverse image and the invariant would not be defined on the intended group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.