mul_one'
plain-language theorem explainer
Right-unit law for the componentwise 2×2 matrix type over Z/3Z that carries Loom traces: X·I = X. Cited when installing the monoid instance on Mat and when proving that opposite letter matrices multiply to the identity. Proof cases on the four entries, reduces each coordinate by simp, and finishes with ring.
Claim. Let $X$ be a $2\times 2$ matrix with entries in $\mathbb{Z}/3\mathbb{Z}$. Then $X\cdot I = X$, where $I$ is the identity matrix and $\cdot$ is ordinary matrix multiplication (implemented entrywise on the four components).
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window forced by the T0–T8 chain. Closed walks up to free reduction and simultaneous conjugation form the content; the computable invariant reads traces (and pairwise commutator traces) in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, because trace is a class function so conjugation-blindness is a ring identity.
Mat is that carrier: a four-field record $(a,b,c,d)$ over ZMod 3, kept as components rather than Matrix so thousands of kernel products reduce cheaply. Multiplication and the unit matrix are defined entrywise; this theorem is the right-unit half of the monoid laws on that type.
Parallel right-unit lemmas exist for the logic-native naturals, integers, rationals, and reals in the foundation stack; they are the same algebraic fact at each layer, not inputs to this proof.
proof idea
Term-mode proof by structure cases. Destructure $X$ into its four ZMod 3 components. Apply the componentwise equality constructor eq_of with four goals. On each goal, simp only [mul, one] unfolds matrix multiplication and the identity matrix to polynomial expressions in the entries, then ring closes the identity over ZMod 3. No external monoid lemma is invoked; the foundation mul_one family is only the same pattern one layer down.
why it matters
Installs mul_one in the Monoid Mat instance alongside mul_assoc' and one_mul', so ordinary monoid rewriting is available on the Loom trace carrier. Downstream, letterMat_mul_neg uses it (with the monoid notation) to show that a table letter and its opposite multiply to the unit matrix, which is the local invertibility step for reduced words in the free group of rank five.
That monoid structure underwrites the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ trace invariant: closed recognition walks on the eight-tick octave are read as matrix words, and the unit law is the base case that empty or cancelled syllables contribute the identity. It does not itself touch the free-group rank $E-V+1=5$ or the depth-two commutator enrichment; those sit higher in Loom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.