tr_mul_comm

Loom certifies configurations of closed recognition walks on the eight-state, three-axis window forced by the Recognition chain. Finished utterances are finite lists of words in the free group of rank five; the module supplies a total well-formedness checker and a computable invariant blind to free reduction and simultaneous conjugation.

Matrices are four-component structures over $\mathbb{Z}/3\mathbb{Z}$ (not Mathlib Matrix), so thousands of products reduce cheaply in the kernel. Trace is the sum of the two diagonal components. Multiplication is ordinary 2-by-2 matrix product, unfolded by a local simp lemma.

Trace is usable here because it is a class function: conjugation blindness is a ring identity rather than a canonicalisation. Loop traces alone collide on some automorphism images, so the invariant also reads pairwise commutator traces.

Destructure both matrix arguments into their four components. Unfold the monoid multiplication and the trace definition via simp, then run the ring tactic on $\mathbb{Z}/3\mathbb{Z}$ to equate the two expanded diagonal sums. No external lemmas beyond the local multiplication and trace unfoldings are required.

This is the elementary class-function identity that makes the Loom invariant blind to conjugation. Downstream, conjugation-invariance of trace rewrites the conjugated product through this commutativity and recovers the original trace when the conjugator has determinant one. The same identity appears when showing that simultaneous reversal of every loop (adjugates) leaves commutator traces unchanged: reversing loops cannot be seen by any trace, because in this group the inverse is the adjugate.

In the Recognition framing the invariant separates closed-walk configurations up to free reduction and the 48 automorphisms of the window; conjugation blindness is deliberately a ring fact, not a search or normal-form step.