mul_assoc'
plain-language theorem explainer
Matrix multiplication on the four-entry Z/3Z carrier used by Loom is associative. Anyone composing loop images or commutators for the SL(2,F_3) trace invariant cites this. The proof cases on the three structures and discharges the four entry equations by ring arithmetic.
Claim. Let $X,Y,Z$ be $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$. Then $(XY)Z = X(YZ)$, where multiplication is the usual bilinear product of matrix entries.
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 module supplies a total well-formedness checker and a computable invariant blind to those two non-content operations.
The invariant evaluates images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and reads ordinary traces plus traces of pairwise commutators (depth-two lower-central data). The carrier is the four-field structure Mat with entries in ZMod 3, kept as components rather than a matrix type so that thousands of kernel products reduce cheaply.
Multiplication of these carriers is the ordinary $2\times 2$ product. Associativity is the algebraic identity needed before longer products of loop images and commutators can be rearranged freely.
proof idea
Term-mode proof. Destructure $X$, $Y$, and $Z$ by cases so each is a four-tuple of ZMod 3 entries. Invoke the componentwise equality lemma eq_of with four goals, one per entry of the product. On each goal, unfold mul and finish by ring on $\mathbb{Z}/3\mathbb{Z}$. No external lemmas beyond that equality helper and the ring tactic.
why it matters
Loom's invariant is a class function on products of loop matrices in $\mathrm{SL}(2,\mathbb{F}_3)$. Without associativity, multi-factor products of generators and their commutators cannot be parenthesized stably, so the certificate checker and the blindness theorems for free reduction and conjugation have no algebraic footing.
Locally it feeds mul_one' in the same module (unit laws for the same carrier). In the broader Recognition stack it sits under the Loom certificate layer that witnesses closed recognition histories on the eight-tick window (forcing chain T7), not under the number-from-logic towers that happen to reuse the same lemma name.
It is pure ring algebra: no open phenomenological hypothesis remains on this line after Loom.BasepointForced removed the old conjugation premise from the load path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.