eq_of
plain-language theorem explainer
Componentwise extensionality for the hand-rolled 2×2 matrices over ℤ/3ℤ used by the Loom invariant: equal entries imply equal matrices. Every algebraic identity in the SL(2, ℤ/3ℤ) certificate layer cites it to reassemble four ring goals into a single matrix equality. The proof is pure structure elimination plus substitution and reflexivity.
Claim. Let $X,Y$ be $2\times 2$ matrices with entries in $\mathbb{Z}/3\mathbb{Z}$, written componentwise as $(a,b;c,d)$. If $X$ and $Y$ agree in every entry, then $X=Y$.
background
The Loom module is a certificate language for 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 of a finished utterance; the computable invariant that ignores exactly those two non-content operations reads traces (and pairwise commutator traces) in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
Rather than Mathlib's Matrix, the module uses a four-field structure Mat with components $a,b,c,d:\mathbb{Z}/3\mathbb{Z}$. The doc-comment states the reason: later evaluation of several thousand products inside the kernel, where Finset.sum does not reduce cheaply. All subsequent matrix algebra (multiplication, adjugate, determinant, units) is therefore written by hand on these four fields.
Because equality of structures is not definitionally componentwise in the way tactics need, every identity proof ends by invoking this extensionality lemma to glue four scalar equalities back into one matrix equality.
proof idea
Term-mode structure elimination. Destructure both matrices with cases, substitute the four component hypotheses, and close by rfl. No external lemmas are required; the argument is pure inductive equality of records.
why it matters
This is the reassembly step for the entire hand-rolled matrix algebra that underwrites the Loom invariant. Downstream it is cited by adj_adj, adj_mul (the key identity that keeps conjugation arguments short), both one-sided Cayley identities mul_adj_of_det_one and adj_mul_of_det_one (so matrices of determinant one are units via the adjugate), and the monoid laws mul_assoc', mul_one', one_mul'. Without it, every ring identity on components would stall before becoming a matrix theorem.
In the Recognition framework the Loom invariant is the trusted checker that a finished configuration of closed walks is well-formed and content-blind; the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ reading (traces plus depth-two commutators) is what separates the intended witness after the free-group rank-5 description of the eight-tick window. Componentwise extensionality is scaffolding for that algebra, not a physics claim, but every certificate identity depends on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.