matAt
plain-language theorem explainer
Indexed lookup on a generator table: the nth pair of matrices (image of a generator and of its inverse) in SL(2,Z/3Z), or the identity pair if the index is out of range. Anyone reading letter images or substitution tables cites it. The body is a three-clause structural recursion on the list and the natural index.
Claim. Given a table $T$ (a list of pairs of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, one pair per generator: image and inverse image) and an index $n\in\mathbb{N}$, return the $n$th pair if it exists, and $(\mathrm{Id},\mathrm{Id})$ otherwise.
background
The Loom module is a certificate language for 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 reduced 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 hand-rolled $2\times 2$ matrix over $\mathbb{Z}/3\mathbb{Z}$ (components rather than Matrix, so kernel evaluation of thousands of products stays cheap). A Table is a list of pairs of such matrices: for each generator, the matrix it maps to and the matrix its inverse maps to. This definition is the pure list-index accessor into that table.
proof idea
Definition by structural recursion, not a proof. Empty table yields the identity pair for any index. Head of a nonempty table is returned at index zero. Successor indices drop the head and recurse on the tail. No lemmas are applied; the three match arms are the entire content.
why it matters
Every letter-to-matrix reading in the Loom invariant goes through this accessor. Downstream, letterMat selects the first or second component of matAt T (|x|-1) according to the sign of the generator letter, and defaults to the identity on zero. entryOk_matAt shows that a well-formed table yields well-formed pairs at every index, so the checker composes. matAt_tableOfSubst identifies lookup after a substitution table with evaluation of the substituted words, which is the bridge from generator images to word images under free-group homomorphisms into $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
In the broader Recognition picture this sits under the eight-tick octave and the free-group certificate layer: the invariant that separates configurations up to the two non-content operations (reduction and basepoint change) is built from traces of these matrix images and their commutators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.