tr_adj
plain-language theorem explainer
Trace on 2-by-2 matrices over Z/3Z is unchanged by the adjugate map. Anyone building or citing the Loom configuration invariant needs this identity: loop reversal is implemented by adjugates, and the invariant must be blind to that gauge move. The proof is a three-line term argument: case-split the four components, unfold, and cancel with ring.
Claim. For every $2\times 2$ matrix $X$ with entries in $\mathbb{Z}/3\mathbb{Z}$, $\operatorname{tr}(\operatorname{adj} X)=\operatorname{tr} X$, where $\operatorname{adj}\begin{pmatrix}a&b\\c&d\end{pmatrix}=\begin{pmatrix}d&-b\\-c&a\end{pmatrix}$ and $\operatorname{tr}$ is the sum of the diagonal entries.
background
Loom is a certificate language for finished 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; the module supplies a total well-formedness checker and a computable invariant that is blind exactly to those two non-content operations.
Matrices are stored as four components a,b,c,d in $\mathbb{Z}/3\mathbb{Z}$ rather than as a library Matrix, so thousands of products reduce cheaply in the kernel. The adjugate is the total map $(a,b,c,d)\mapsto(d,-b,-c,a)$; on the determinant-one subgroup it is the group inverse. Trace is the class function $a+d$, which is why conjugation-blindness is a ring identity rather than a canonicalisation step.
The invariant reads traces of the loop images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ together with traces of their pairwise commutators (depth-two lower-central data). Loop traces alone collide on some automorphism images, so the commutator layer is required.
proof idea
Term-mode, three steps. Case-split the structure Mat into its four fields. Unfold the definitions of adjugate and trace, so the goal is $d+a=a+d$ in $\mathbb{Z}/3\mathbb{Z}$. Finish with ring. No external lemmas are required beyond the local definitions of adj and tr.
why it matters
Feeds invariantOf_adj: reversing every loop at once (mapping each matrix to its adjugate) leaves the Loom invariant unchanged, with no extra hypothesis. Downstream doc-comment: "in the determinant one subgroup the inverse is the adjugate, and no trace can see an adjugate. So the gate's hostile choice, putting time reversal into the gauge group, costs the carrier nothing."
That closes one of the two blindness theorems the module exists to prove. Trace is a class function, so conjugation-blindness is algebraic; adjugate-blindness of the diagonal sum is the matching algebraic fact for orientation reversal. Together they let the invariant treat free reduction and gauge moves as non-content while still separating the intended witness via commutator traces. Sits inside the Loom certificate layer on the eight-tick window (T7), not in the forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.