Mat
plain-language theorem explainer
Four-component carrier for 2×2 matrices over Z/3Z, the ring in which Loom evaluates its closed-walk invariant. Anyone citing the SL(2,F3) trace or commutator-trace certificate depends on this type. It is a bare structure (not Mathlib Matrix) so that thousands of kernel products reduce without Finset.sum overhead.
Claim. A matrix is a 4-tuple $(a,b,c,d)$ with each entry in $\mathbb{Z}/3\mathbb{Z}$, representing $\begin{pmatrix} a & b \\ c & d \end{pmatrix}$. Equality and printing are decidable.
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 homotopy form a free group of rank five; a configuration is a finite list of reduced words sharing a basepoint. Content is quotiented by free reduction and by simultaneous conjugation, so the checker needs a conjugation-blind invariant.
That invariant is built from traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Trace is a class function, so blindness to conjugation is a ring identity rather than a normal-form computation. Loop traces alone collide on some automorphism images, so the invariant also records traces of pairwise commutators (depth-two lower-central-series data).
The present declaration is the raw 2×2 matrix type over that field. Components are stored flat rather than as Mathlib Matrix because a later module multiplies several thousand of them inside the kernel, where Finset.sum does not reduce cheaply.
proof idea
Definition only: four fields of type ZMod 3, with derived DecidableEq and Repr. No proof body. Downstream arithmetic (multiplication, adjugate, conjugation, determinant) is defined by component formulas and proved by cases plus ring or linear_combination.
why it matters
This is the carrier type for the entire Loom invariant stack. Immediate consumers include the adjugate (adj), conjugation (cj), multiplication, and the identities adj_mul, adj_adj, adj_cj, and adj_mul_of_det_one that make conjugation arguments short without component blow-up. The module doc states the design goal: a total checker and a computable invariant blind exactly to free reduction and simultaneous conjugation, carrying no model or search. The choice of $\mathrm{SL}(2,\mathbb{F}_3)$ sits on the eight-tick, three-axis window (T7–T8 landmarks) where closed walks live; the matrix type is the concrete ring object that makes the class-function argument executable in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.