letterMat_neg
plain-language theorem explainer
Under a well-formed generator table, the matrix image of a negated letter equals the adjugate of the image of the letter. Anyone proving that word inversion becomes matrix adjugation in the Loom SL(2,Z/3Z) evaluation cites this. The proof is a short calc: det=1 turns the identity into adj·M, then the letter–inverse product identity cancels the trailing factors.
Claim. Let $T$ be a well-formed table of generator matrices over $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. For every integer letter $x$, the matrix assigned to $-x$ equals the adjugate of the matrix assigned to $x$: $\rho_T(-x)=\mathrm{adj}(\rho_T(x))$.
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window from the forcing chain. 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})$, including pairwise commutator traces at depth two of the lower central series.
Matrices are stored by four components in $\mathbb{Z}/3\mathbb{Z}$ (not Mathlib Matrix) so thousands of products reduce cheaply in the kernel. A Table is a list of pairs: for each generator, the matrix it maps to and the matrix its inverse maps to. Well-formedness (Table.ok) enforces that these images lie in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ with consistent inverse pairing.
The letter map $\rho_T$ sends a signed generator index to its table matrix. Because $\det=1$, the adjugate coincides with the group inverse, which is why adjugation is the right algebraic image of letter inversion.
proof idea
First obtain $\det(\rho_T(x))=1$ from det_letterMat (using well-formedness) and the product identity $\rho_T(x),\rho_T(-x)=1$ from letterMat_mul_neg.
Rewrite $\rho_T(-x)$ as $1\cdot\rho_T(-x)$, replace the leading $1$ by $\mathrm{adj}(\rho_T(x)),\rho_T(x)$ via Mat.adj_mul_of_det_one, reassociate, then cancel the trailing product against the product identity and right-multiply by one. The only essential use of determinant one is that adjunction step.
why it matters
This is the letter-level seed for evalWord_invWord: evaluation of an inverted word equals the adjugate of the evaluation of the original word, proved by induction on the word using this fact at each cons step. That homomorphism property is what lets free reduction and inversion act as matrix identities rather than as syntactic rewrites when the Loom invariant reads traces and commutator traces.
In the broader Recognition setting the invariant must be blind exactly to the two non-content operations (free reduction; simultaneous conjugation). Trace is already a class function; letter-to-adjugate supplies the inversion half of free-group duality inside $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. The module doc notes this is the only place the determinant-one hypothesis is really used, so the SL condition is not decorative scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.