det_adj
plain-language theorem explainer
For every 2×2 matrix over ℤ/3ℤ, the determinant of its classical adjugate equals the determinant of the matrix. Loom invariant proofs cite this when identifying word-inverses with adjugates inside SL(2, ℤ/3ℤ). The argument is a short algebraic identity: split the four entries, unfold adj and det, and finish by ring.
Claim. Let $X$ be a $2\times 2$ matrix with entries in $\mathbb{Z}/3\mathbb{Z}$. Then $\det(\mathrm{adj}\, X)=\det X$, where $\mathrm{adj}$ is the classical adjugate.
background
The Loom module treats finished recognition histories as finite lists of freely reduced words in five signed generators (the free group of rank $E-V+1=5$ on the eight-state, three-axis window). Content is what survives free reduction and simultaneous conjugation; the module supplies a total well-formedness checker and a computable invariant that is blind to exactly those two operations.
Matrices are the hand-rolled four-component structure Mat over $\mathbb{Z}/3\mathbb{Z}$, not Mathlib Matrix, so that later kernel evaluation of thousands of products stays cheap. The invariant lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$: loop images are required to have determinant one, and the inverse of a unit-determinant matrix is its classical adjugate. Trace is a class function, so conjugation-blindness is a ring identity; pairwise commutator traces supply the depth-two data that pure abelianisation would erase.
For $2\times 2$ matrices the general identity $\det(\mathrm{adj}, X)=(\det X)^{n-1}$ specialises to $\det(\mathrm{adj}, X)=\det X$, which is what this lemma records over the residue ring.
proof idea
Term-mode proof by cases on the four-component structure. After cases X, both sides are polynomials in the four entries $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$. Unfolding the local definitions of adjugate and determinant reduces the goal to an equality of two explicit cubic polynomials; ring discharges it. No external lemmas are required beyond the component definitions of adj and det.
why it matters
Downstream, ok_tableOfSubst preserves table well-formedness under substitution. Its proof needs that every evaluated generator word has determinant one and that the evaluation of the inverse word is exactly the adjugate of the evaluation; det_adj is the algebraic hinge that keeps those two facts compatible when determinants are compared after inversion.
In the broader Loom story this is bookkeeping for the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ reading of closed walks. The module claims no model and no search: it only certifies finished objects. The forcing-chain landmarks that fix the window (eight-tick octave, $D=3$) sit upstream of the free-group rank count; this lemma does not re-prove them, but it is part of the certificate layer that makes the invariant trustworthy once those landmarks are granted.
Without $\det(\mathrm{adj}, X)=\det X$, the identification of geometric inverse with adjugate would not automatically preserve the $\mathrm{SL}$ condition, and the substitution-stability theorem would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.