letterMat
plain-language theorem explainer
Maps a signed generator index to its matrix image in SL(2, Z/3Z) under a fixed generator table. Positive letters take the forward matrix, negative letters the stored inverse, and zero the identity. Downstream word evaluation and determinant checks cite it as the atomic letter homomorphism. The body is a three-way case split on the sign of the integer.
Claim. Given a generator table $T$ (a list of pairs of $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$) and an integer letter $x$, return the matrix image of that letter: if $x>0$, the first component of the $(|x|-1)$-st table entry; if $x<0$, the second component of that entry; if $x=0$, the identity matrix.
background
Loom is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window. 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. The module supplies a total well-formedness checker and a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, blind to free reduction and simultaneous conjugation.
Mat is a four-component record $(a,b,c,d)$ over $\mathbb{Z}/3\mathbb{Z}$, used instead of a matrix type so that thousands of products reduce cheaply in the kernel. A Table is a list of pairs of such matrices: for each generator, the image of the generator and the image of its inverse. Lookup is by matAt, which returns the pair at a natural index (or the identity pair on overflow).
Signed letters are integers: positive $k$ means generator $k$, negative $-k$ its inverse, and zero is treated as the empty contribution (identity).
proof idea
Definition by cases on the sign of $x$. When $0<x$, take the first projection of matAt T (|x|-1). When $x<0$, take the second projection of the same lookup (the stored inverse). Otherwise return Mat.one. No lemmas are applied; the body is pure case analysis and projection.
why it matters
This is the atomic letter map for the Loom representation. Word evaluation is defined by left-folding it: evalWord T (x :: t) = letterMat T x * evalWord T t, with singleton and reduced-cons variants following immediately. Determinant preservation (det_letterMat) uses the table well-formedness hypothesis to show every letter lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Substitution lemmas rewrite letter images under table morphisms via the same case split.
In the Recognition framework the Loom invariant separates closed-walk configurations up to the two non-content operations (free reduction and basepoint conjugation). The letter map is the bridge from free-group spelling to the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ traces and commutator traces that form that invariant. It sits downstream of the eight-tick octave and free-group rank $E-V+1=5$ forced by the T0–T8 chain, but carries no model of its own.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.