det
plain-language theorem explainer
Classical 2×2 determinant over ℤ/3ℤ on the componentwise matrix type used by Loom. Anyone working the SL(2, ℤ/3ℤ) trace invariant of closed recognition walks cites it: special-linear matrices are exactly those with this determinant equal to one. The body is the four-entry formula ad−bc, not a Mathlib Matrix call.
Claim. For a $2\times 2$ matrix $X$ with entries $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$, the determinant is $\det(X)=ad-bc\in\mathbb{Z}/3\mathbb{Z}$.
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. Closed walks up to free reduction and simultaneous conjugation are words in a free group of rank five; the module supplies a total well-formedness checker and a computable invariant blind to those two non-content operations.
The invariant is built from traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Matrices are stored as an explicit four-field structure Mat (components $a,b,c,d$ in $\mathbb{Z}/3\mathbb{Z}$) rather than Mathlib Matrix, so that later kernel evaluations of thousands of products stay cheap. Trace is a class function, so conjugation-blindness is a ring identity. Loop traces alone collide on some automorphism images, so the invariant also reads traces of pairwise commutators (depth-two lower-central data).
This determinant is the scalar that cuts out the special-linear locus: every matrix the module actually evaluates is required to have determinant one, which is exactly when the adjugate acts as a two-sided inverse.
proof idea
Pure definition: expand $\det$ as the ring expression $a\cdot d-b\cdot c$ on the four components of Mat. No lemmas, no tactics, no Mathlib determinant API.
why it matters
Without a cheap, total determinant on the component matrix type, Loom cannot state the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ side condition that makes the adjugate an inverse and makes traces well-defined class functions on the image of reduced words. That condition is what lets the configuration invariant ignore simultaneous conjugation (a ring identity) while still separating witnesses that pure abelianised loop traces miss.
Downstream, the same scalar appears wherever Loom certificates or related constant-boundary audits need a nonzero or unit determinant check (dimensional boundary matrices for $(c,\hbar,G)$, Hessian nondegeneracy in cost coordinates, and κ-blind closure arguments that refuse to pin couplings by ledger combinatorics alone). In the broader Recognition chain it sits under the eight-tick octave (T7) and the $D=3$ window (T8): the finite ring $\mathbb{Z}/3\mathbb{Z}$ is the arithmetic shadow of that discrete register, not an arbitrary modulus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.