adj
plain-language theorem explainer
Adjugate on the hand-rolled 2×2 matrices over ℤ/3ℤ used by Loom: [[a,b],[c,d]] maps to [[d,-b],[-c,a]]. Anyone reading SL(2,ℤ/3ℤ) images of closed recognition walks cites it to invert group elements. One-line component constructor; total, and equals the inverse exactly when det = 1.
Claim. For a matrix $X=\begin{pmatrix}a&b\\c&d\end{pmatrix}$ with entries in $\mathbb{Z}/3\mathbb{Z}$, define $\operatorname{adj}(X)=\begin{pmatrix}d&-b\\-c&a\end{pmatrix}$. This is a total function on the component structure; it is the two-sided inverse of $X$ precisely when $\det X=1$.
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 are words in a free group of rank 5; the module's invariant reads their images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ via traces and pairwise commutator traces.
Matrices are the component structure Mat with four fields $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$, not Mathlib's Matrix, so that later kernel evaluations of thousands of products stay definitionally cheap. The classical adjugate of $\begin{pmatrix}a&b\c&d\end{pmatrix}$ is exactly $\begin{pmatrix}d&-b\-c&a\end{pmatrix}$. The doc-comment records that every matrix this module evaluates has determinant one, so adjugate coincides with inverse on the image.
proof idea
Pure definition: construct the four-tuple $\langle X.d,,-X.b,,-X.c,,X.a\rangle$ from the input components. No lemmas, no tactics.
why it matters
Supplies the inverse operation inside Loom's $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ calculus. Trace is a class function, so conjugation-blindness is a ring identity; products and inverses of loop images are needed both for the loop traces and for the depth-two commutator traces that separate automorphism images the abelianised reading collides on. Without a total, componentwise adjugate the invariant checker could not stay computable and free of Mathlib matrix overhead. Feeds every downstream site that multiplies by an inverse or checks reduced words against their matrix images. Landmark link: the eight-tick octave and $D=3$ fix the window whose closed walks this certificate language reads.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.