tr_cj

The Loom module treats finished recognition histories as finite lists of reduced words in a free group of rank five (closed walks on the eight-state, three-axis window). Content is defined by two refusals: free reduction (spelling is not content) and simultaneous conjugation of every loop by one common word (basepoint is not content). The computable invariant that witnesses both refusals evaluates loop images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ and records ordinary traces together with traces of pairwise commutators.

Mat is a hand-rolled $2\times 2$ matrix over $\mathbb{Z}/3\mathbb{Z}$ (four components $a,b,c,d$), chosen so that thousands of products reduce inside the kernel without Finset.sum. Conjugation is cj G X := G * X * adj G; under $\det G=1$ the adjugate is the inverse, so this is ordinary group conjugation in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Trace is the sum of the diagonal entries. The module header states the design reason directly: "Trace is a class function, which is the whole reason it is usable here: blindness to conjugation is a ring identity rather than a canonicalisation."

First obtain adj G * G = 1 from the standing hypothesis det G = 1 via adj_mul_of_det_one. Then a four-step calc:

1. Unfold cj and reassociate to tr(G * (X * adj G)).
2. Apply the cyclic identity tr_mul_comm to rotate the leading $G$ to the right, getting tr(X * adj G * G).
3. Reassociate the product inside the trace to tr(X * (adj G * G)).
4. Substitute adj G * G = 1 and cancel with mul_one, leaving tr X.

No case splits on entries; the argument is pure ring algebra on the matrix monoid.

This is the ring-level fact that makes the Loom invariant basepoint-blind. Downstream, invariantOf_cj ("THE SOUNDNESS THEOREM. There is no first word") maps the identity across every loop of an utterance and concludes that conjugating the whole configuration by one $G\in\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ leaves the invariant unchanged. The companion trN_conjWord uses the same identity to show that nesting a loop inside a binder is invisible at depth one: "a loop that sits inside a binder is a CONJUGATE of the same loop outside it, and a trace cannot see a conjugation."

In the broader Recognition picture the Loom sits on the eight-tick octave (forcing step T7) and the free group of closed walks on the three-axis window (T8 forces $D=3$). Trace-class-function status is what lets the certificate language avoid choosing a basepoint, matching the module's claim that a closed history is a map from a circle and names no vertex as first. Without this lemma the depth-one half of the invariant would have to canonicalise words rather than evaluate them.