one_def
plain-language theorem explainer
The multiplicative unit on the componentwise 2×2 matrix type over ℤ/3ℤ equals the explicit identity matrix constructor. Anyone proving determinant or adjugate identities for SL(2, ℤ/3ℤ) matrix images of loom words cites this. The proof is pure reflexivity from the OfNat instance.
Claim. Writing $M$ for the type of $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$ given by four components, the multiplicative identity $1:M$ equals the explicit identity matrix (diagonal ones, off-diagonal zeros).
background
Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to free reduction and simultaneous conjugation form the content; the computable invariant reads traces (and pairwise commutator traces) of loop images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
Rather than Mathlib's Matrix, the module uses a four-component structure Mat with entries in ZMod 3, so that thousands of products reduce cheaply inside the kernel. The multiplicative monoid structure on Mat supplies an OfNat instance whose value at $1$ is an explicit identity record (ones on the diagonal, zeros off it). This theorem simply names that definitional equality.
proof idea
One-line reflexivity. The OfNat instance for Mat defines the numeral $1$ to be the explicit identity record, so (1 : Mat) = one holds by rfl with no further lemmas.
why it matters
Downstream determinant and invertibility lemmas unfold through this equality: det_one shows $\det(1)=1$; mul_adj_of_det_one and adj_mul_of_det_one show that when $\det X=1$, the adjugate is a two-sided inverse, writing the right-hand side as $1$ via this definition. Those identities feed the well-formedness preservation theorem for substitution tables (ok_tableOfSubst), which needs that word images stay in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and that inverse words evaluate to adjugates.
In the Recognition framework this sits inside the Loom certificate layer for closed walks on the eight-tick window (forcing chain T7). Trace is a class function, so conjugation-blindness is a ring identity; the unit matrix is the base case of every such calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.