det_one
plain-language theorem explainer
The identity matrix among Loom's componentwise 2×2 matrices over ℤ/3ℤ has determinant 1. Anyone showing that evaluated closed-walk words land in SL(2, ℤ/3ℤ) cites this as the empty-word base case. Unfolding the identity and determinant definitions reduces the claim to ring arithmetic on four entries.
Claim. For the componentwise $2\times 2$ matrix type over $\mathbb{Z}/3\mathbb{Z}$, $\det(I)=1$, where $I$ is the multiplicative identity matrix.
background
Loom is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to free reduction and simultaneous conjugation are words in a free group of rank 5; the module supplies a total well-formedness checker and a computable invariant blind to those two non-content operations.
The invariant reads traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Matrices are stored as a four-component structure Mat (entries $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$) rather than Mathlib's Matrix, so thousands of products inside the kernel reduce without Finset.sum. The determinant is the usual $ad-bc$ on those components; the multiplicative unit is the matrix with $1$s on the diagonal and $0$s off it.
Membership in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ means determinant exactly $1$. Trace is a class function, so conjugation-blindness is a ring identity; pairwise commutator traces supply the depth-two data that pure loop traces fail to separate.
proof idea
One short tactic proof. simp only unfolds the identity-matrix definition (diagonal ones, off-diagonal zeros), the one instance, and the four-entry determinant formula $ad-bc$. The resulting equality of elements of $\mathbb{Z}/3\mathbb{Z}$ is discharged by ring.
why it matters
This is the empty-word base of the SL-membership chain for the Loom invariant. Downstream, det_evalWord inducts on words: the nil case is exactly this theorem, and the cons step multiplies by det_letterMat (each generator image also has det 1) using multiplicativity of det. Together they prove every evaluated word has determinant 1, so the configuration invariant genuinely lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ rather than $\mathrm{GL}$.
In the Recognition framework the eight-tick window (T7) and $D=3$ (T8) fix the discrete geometry whose closed walks the Loom certifies. Without det-one, the induction that the invariant is well-defined on reduced words would have no base, and the claim that the certificate is blind to conjugation via class functions would not sit inside a group of determinant-one matrices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.