one_mul'
plain-language theorem explainer
Left unit law for the custom 2×2 matrix type over Z/3Z that carries Loom traces: identity times X equals X. Cited wherever the monoid structure on Mat is assembled (right-unit twin, Mul/One instances, configuration invariants). Proof is a four-goal componentwise reduction via eq_of, then simp and ring.
Claim. Let $X$ be a $2\times 2$ matrix with entries in $\mathbb{Z}/3\mathbb{Z}$. Then $I\cdot X = X$, where $I$ is the identity matrix and $\cdot$ is the componentwise matrix product on this carrier.
background
Loom certifies finished 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 computable invariant reads matrix traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, including pairwise commutator traces so that abelianised readings do not collide.
Mat is that carrier: four fields $a,b,c,d\in\mathbb{Z}/3\mathbb{Z}$, kept as a plain structure rather than Mathlib Matrix so thousands of kernel products reduce cheaply. Multiplication and the identity element are defined componentwise on those fields. Equality of matrices is discharged by the local lemma eq_of, which rebuilds structural equality from four component equalities.
This unit law is the left half of the monoid axioms on that carrier; the module supplies no model or search, only the checker, the invariant, and blindness theorems for the two non-content operations.
proof idea
Term-mode proof after a single cases on the matrix. The goal becomes four component identities. refine eq_of _ _ ?_ ?_ ?_ ?_ splits into those four goals; each is closed by simp only [mul, one] (unfolding the product and identity definitions) followed by ring on $\mathbb{Z}/3\mathbb{Z}$. No external monoid lemma is invoked; the algebra is fully expanded.
why it matters
Loom's invariant is a class function on matrix images of loops, so the carrier must be a monoid (and ultimately sit inside $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$). This lemma is the left unit half of that structure. Its immediate sibling mul_one' is the right unit and is proved identically; together they underwrite the Mul and One instances on Mat.
Downstream, the same naming pattern appears in the logic-derived integer, rational, and real stacks and in the PRC rational-field certificate, which packages unit laws into a field certificate. Inside Loom the unit laws keep reduced words and conjugated configurations from shifting traces when an identity factor is inserted, which is required for the invariant to be blind exactly to free reduction and simultaneous conjugation.
No forcing-chain step (T5–T8) is proved here; the link is infrastructural: the eight-tick window supplies the $\mathbb{Z}/3\mathbb{Z}$ coefficients, and this monoid law makes the trace reading well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.