det_mul
plain-language theorem explainer
Determinant is multiplicative for the componentwise 2×2 matrices over ℤ/3ℤ used by the Loom certificate language. Anyone checking that products of loop images stay in SL(2, ℤ/3ℤ), or that the trace invariant is well-defined on words, cites this. The proof expands both factors, unfolds the explicit product and determinant formulas, and finishes by ring arithmetic.
Claim. Let $X,Y$ be $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$, written by components $(a,b,c,d)$. Then $\det(XY)=\det(X)\,\det(Y)$, where multiplication and determinant are the usual formulas on those four entries.
background
Loom 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). The module's computable invariant maps those words into $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and reads traces of the images and of their pairwise commutators.
Mat is not Mathlib's Matrix: it is a four-field structure over ZMod 3 so that thousands of products reduce cheaply in the kernel. Multiplication and determinant are therefore explicit polynomials in the four entries. Multiplicativity of det is the elementary ring identity that keeps the special-linear condition closed under word evaluation and under the products that appear when forming commutators.
proof idea
Term-mode proof by cases on the two Mat values, exposing the four components of each. simp unfolds the local definitions of matrix multiplication and of the determinant polynomial. The resulting equality of polynomials in eight variables over $\mathbb{Z}/3\mathbb{Z}$ is discharged by ring. No external lemmas are required.
why it matters
The Loom invariant is built so that spelling (free reduction) and simultaneous conjugation are invisible; trace is a class function, and det-multiplicativity is the companion identity that keeps every evaluated word inside $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Without it, the certificate checker could not trust products of loop images or the depth-two commutator data that separates automorphism orbits the plain traces miss.
In the broader Recognition chain this sits under the eight-tick, three-axis window (T7–T8): closed walks on that window are the objects Loom certifies. The lemma is pure linear algebra over a three-element ring; its place in the framework is infrastructural rather than a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.