mul

Loom is a certificate language for finished configurations of closed recognition walks on the eight-state, three-axis window from the forcing chain. Closed walks up to homotopy form a free group of rank five; a finished utterance is a finite list of reduced words sharing a basepoint. The module supplies a well-formedness checker and a computable invariant blind to free reduction and simultaneous conjugation.

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). Matrices are the local structure Mat: four components $a,b,c,d:\mathbb{Z}/3\mathbb{Z}$, chosen instead of Mathlib Matrix because a later module multiplies several thousand products inside the kernel and Finset.sum does not reduce cheaply.

Pure definition: the four entries of the ordinary $2\times 2$ product over the ring $\mathbb{Z}/3\mathbb{Z}$, written as a structure constructor. No lemmas, no tactics.

Multiplication is the monoid operation that turns generator images into word images before the Loom invariant reads traces. Trace is a class function, so conjugation-blindness is a ring identity; products must still be formed explicitly to evaluate each loop and each pairwise commutator. Without a cheap componentwise product, the kernel-side evaluation of thousands of certificates would not reduce. The definition sits under the Loom invariant stack that certifies configurations of closed recognition walks; it carries no model and no search, only the arithmetic the checker needs. No downstream edges are recorded in the current graph snapshot, but every product of loop matrices in this module depends on it.