comm_cj
plain-language theorem explainer
Conjugation by a unit-determinant 2×2 matrix over Z/3Z intertwines with the matrix commutator: the commutator of two conjugates equals the conjugate of the commutator. Anyone proving that the Loom configuration invariant is blind to simultaneous basepoint change cites this identity. The proof is a short algebraic expansion using the conjugation-multiplication law and the fact that conjugation commutes with adjugates.
Claim. Let $G,X,Y$ be $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$ with $\det G=1$. Writing $\mathrm{Ad}_G(M)=G M G^{-1}$ (via the adjugate, which equals the inverse when $\det G=1$) and $[A,B]=A B A^{-1} B^{-1}$, one has $[\mathrm{Ad}_G(X),\mathrm{Ad}_G(Y)]=\mathrm{Ad}_G([X,Y])$.
background
The Loom module is a certificate language for 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 of a finished utterance; the module supplies a total well-formedness checker and a computable invariant blind to those two non-content operations.
Matrices here are the structure Mat: four components in $\mathbb{Z}/3\mathbb{Z}$, used instead of a generic matrix type so that thousands of products reduce inside the kernel. The adjugate is the total map $(a,b;c,d)\mapsto(d,-b;-c,a)$; when $\det=1$ it is the inverse, which is the only case the module evaluates. Conjugation $\mathrm{Ad}_G$ is implemented by left-multiplying by $G$ and right-multiplying by that adjugate. The commutator is the usual word $XYX^{-1}Y^{-1}$ in this monoid.
The invariant reads traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ of the loop images and of their pairwise commutators (depth-two lower-central data). Trace is a class function, so conjugation-blindness is a ring identity; the commutator half of that identity is exactly this lemma.
proof idea
Term-mode proof in two steps. First unfold the commutator definition and apply the sibling fact that conjugation commutes with adjugates, so each inverse factor becomes an adjugate of a conjugate. Then rewrite three times with the conjugation-multiplication identity (valid under $\det G=1$): once on $X Y$, once on $\mathrm{adj}(X),\mathrm{adj}(Y)$, and once on the product of those two blocks. The resulting expression is exactly conjugation applied to the original commutator.
why it matters
Parent theorem is invariantOf_cj, the soundness theorem: simultaneous conjugation of every loop matrix by the same unit-determinant $G$ leaves the configuration invariant unchanged. That proof needs both that traces of conjugates equal traces, and that the pairwise-commutator traces transform the same way; this lemma supplies the second half by pushing conjugation inside each commutator before taking trace.
In the Loom story this closes the basepoint-blindness half of content: a closed history is a map from a circle and names no preferred vertex, so conjugating every generator by one fixed word must not change the certificate. The module doc stresses that loop traces alone collide on automorphism images, which is why commutator traces are part of the invariant; without the present identity that extra data would not inherit conjugation invariance. Framework-wise this sits under the eight-tick octave and free-group rank $E-V+1=5$ geometry of closed recognition walks, not under the J-cost or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.