det_letterMat
plain-language theorem explainer
Every generator letter, under a well-formed Loom table, lands in SL(2, Z/3Z): its image matrix has determinant 1. Anyone proving that word evaluation stays in the special linear group cites this. The proof case-splits on the sign of the letter and reads the det=1 clauses already stored in the table well-formedness predicate.
Claim. Let $T$ be a finite list of matrix pairs over $\mathbb{Z}/3\mathbb{Z}$, each pair intended as a generator image and its inverse. If every pair multiplies to the identity in both orders and both matrices have determinant $1$, then for every integer letter $x$ the matrix assigned to $x$ satisfies $\det=1$.
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to free reduction and simultaneous conjugation form the content; the module supplies a total well-formedness checker and a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
Matrices here are explicit $2\times 2$ records over $\mathbb{Z}/3\mathbb{Z}$ (components $a,b,c,d$), not Mathlib Matrix, so kernel evaluation of long products stays cheap. Determinant is $ad-bc$. A table is a list of pairs $(M,M^{-1})$; entryOk demands both products equal the identity and both determinants equal $1$. The letter map sends a positive index to the first matrix of the corresponding pair, a negative index to the second, and zero to the identity.
Upstream, entryOk_matAt lifts table-wide well-formedness to every index: the pair at position $n$ really is an inverse pair inside the determinant-one subgroup.
proof idea
Apply entryOk_matAt at index $|x|-1$ and unpack the Boolean conjunction to obtain the four equalities (mutual inverses and both determinants $1$). Unfold the letter map and case on the sign of $x$.
If $x>0$, the letter map selects the first matrix of the pair; its determinant clause is exactly the goal. If $x<0$, the second matrix is selected and the other determinant clause finishes it. If $x=0$, the letter map is the identity matrix, and det_one gives $\det I=1$.
why it matters
This is the atomic SL-membership fact for single letters. Downstream, det_evalWord inducts along a word, multiplying determinants via the multiplicative formula and invoking this lemma at each cons step, so every evaluated word lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. The companion letterMat_neg uses the same fact to identify the image of $-x$ with the adjugate of the image of $x$ (the only place the det$=1$ hypothesis is truly spent).
In the Loom story that matters: the invariant reads traces and pairwise-commutator traces in the special linear group over $\mathbb{Z}/3\mathbb{Z}$. Trace is a class function, so conjugation-blindness is a ring identity. Keeping every letter (hence every word) inside $\mathrm{SL}$ is what makes the adjugate the genuine inverse and keeps the invariant well-defined on free-group elements rather than on raw unreduced strings. The free group of rank $5$ on the eight-tick window (forcing chain T7) is the ambient algebra this representation serves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.