comm
plain-language theorem explainer
Defines the group commutator of two matrices in the Loom SL(2,Z/3Z) representation: XYX^{-1}Y^{-1}, written via adjugates. Anyone building or reading the Loom configuration invariant cites it for the depth-two (lower central series) coordinates. The body is a one-line product of the two matrices with the product of their adjugates.
Claim. For $X,Y\in\mathrm{Mat}$ (componentwise $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$), the commutator is $\mathrm{comm}(X,Y):=XY\,\mathrm{adj}(X)\,\mathrm{adj}(Y)$, i.e. $XYX^{-1}Y^{-1}$ whenever $\det=1$ so that the adjugate is the inverse.
background
Loom 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 homotopy form a free group of rank $E-V+1=5$; a finished utterance is a finite list of such words sharing a basepoint. Content is quotiented by free reduction and by simultaneous conjugation (basepoint indifference).
The computable invariant evaluates loop images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Matrices are stored as a four-component structure Mat over $\mathbb{Z}/3\mathbb{Z}$ (not Mathlib Matrix) so kernel products reduce cheaply. The adjugate adj X = ⟨X.d, -X.b, -X.c, X.a⟩ is total and equals the inverse on every matrix the module evaluates (determinant one).
Plain loop traces are a class function, hence conjugation-blind by a ring identity, but they collide on some of the 48 window automorphisms. The invariant therefore also reads traces of pairwise commutators: the depth-two data of the lower central series, which abelianisation erases.
proof idea
Pure definition: expand as the product $XY(\mathrm{adj},X*\mathrm{adj},Y)$. No lemmas, tactics, or proof obligations. On the $\det=1$ locus used throughout Loom this is exactly the group commutator $XYX^{-1}Y^{-1}$.
why it matters
Module documentation states the design reason: loop traces alone fail to separate the intended witness (they collide on two of the forty-eight automorphism images), so the invariant also consumes traces of pairwise commutators of the loop images. That is precisely the depth-two lower-central-series coordinate; an abelianised reading is blind to it by construction.
The declaration therefore supplies the non-abelian depth that makes the Loom invariant a faithful certificate for finished recognition configurations. Downstream Loom consumers apply it when assembling the multi-loop invariant (trace of each loop image together with traces of all pairwise commutators). It sits inside the certificate layer only: no model, no search, trusted with finished objects it did not build. Framework landmarks: the free group of rank 5 on the eight-tick window (T7) and the conjugation-blindness that matches basepoint indifference after Loom.BasepointForced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.