one

Loom is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain. 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 reads matrix images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. The carrier is not Mathlib's Matrix but a four-field structure Mat with components $a,b,c,d:\mathbb{Z}/3\mathbb{Z}$, chosen so that thousands of kernel products reduce without expensive Finset.sum. Trace is a class function, so conjugation-blindness is a ring identity; pairwise commutator traces supply the depth-two data that pure loop traces fail to separate.

This declaration is simply the monoid unit of that component ring.

One-line definition: the structure constructor applied to the four literals $1,0,0,1$ in $\mathbb{Z}/3\mathbb{Z}$. No lemmas, no tactics.

Supplies the multiplicative unit for every subsequent product, inverse, and trace evaluation inside Loom.Core. The module's invariant (traces of loop images and of their pairwise commutators in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$) is only well-defined once the identity matrix is named; free reduction and conjugation-invariance proofs treat it as the empty-word image. No downstream edges are recorded yet, but the unit is ambient infrastructure for the certificate checker rather than a standalone theorem. It sits under the eight-tick octave and free-group rank $E-V+1=5$ setting of the Loom header, not under a numbered forcing-chain step.