trN_comm_adj
plain-language theorem explainer
The trace of a group commutator is unchanged when both arguments are replaced by their adjugates. Provers of Loom gauge-invariance under simultaneous loop reversal cite this identity. The argument expands both commutators via the anti-homomorphism laws for adjugate, then finishes by the cyclic property of trace.
Claim. For all carrier matrices $X,Y$ (componentwise $2\times 2$ over $\mathbb{Z}/3\mathbb{Z}$), $\operatorname{tr}([\operatorname{adj} X,\operatorname{adj} Y])=\operatorname{tr}([X,Y])$, where $\operatorname{adj}$ is the adjugate (group inverse on the determinant-one locus) and $[A,B]=AB\,\operatorname{adj}(BA)$.
background
Loom certifies finished configurations of closed recognition walks on the forced eight-state, three-axis window. Content is a finite list of freely reduced words in the rank-five free group of based loops, read up to simultaneous conjugation. The computable invariant lands in traces over the determinant-one matrices in $M_2(\mathbb{Z}/3\mathbb{Z})$.
Matrices are stored as the four-component structure Mat rather than Mathlib Matrix, so thousands of products reduce cheaply in the kernel. On the determinant-one locus the group inverse is exactly the adjugate. Plain loop traces are conjugation-invariant (trace is a class function) but collide on some of the forty-eight window automorphisms, so the invariant also records traces of pairwise commutators: the depth-two lower-central-series data that abelianization destroys.
Simultaneous reversal of every loop is the remaining candidate gauge move. Because reversal is adjugation in this group, blindness of every trace (loop or commutator) to adjugation is the algebraic content of that gauge choice.
proof idea
Two short expansions, then one cyclic identity. Rewrite the commutator of the adjugates by unfolding the commutator definition together with adj_adj (involution) and adj_mul (anti-homomorphism) and reassociating, obtaining $\operatorname{adj}(YX)\cdot(XY)$. Rewrite the plain commutator the same way as $(XY)\cdot\operatorname{adj}(YX)$. Apply the cyclic law $\operatorname{tr}(AB)=\operatorname{tr}(BA)$ to the first product; both sides become the same trace.
why it matters
The sole downstream consumer is invariantOf_adj, which lifts the pairwise identity to the full configuration invariant: mapping every matrix in the list by adjugate leaves the invariant unchanged. Its doc-comment states the point directly: the gate may put time reversal into the gauge group at no cost to the carrier, because no trace can see an adjugate.
Together with free reduction and basepoint conjugation (the latter now theorem-backed by rotate_is_conjugation plus the same label-blindness that quotients by the 48 window automorphisms), this closes the two non-content operations the Loom checker is required to ignore. It sits inside the eight-tick, rank-five free-group picture of closed walks on the forced window without itself invoking the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.