tr
plain-language theorem explainer
The Loom matrix trace on 2×2 matrices over Z/3Z is the sum of the two diagonal entries. Anyone building or checking the Loom configuration invariant (class functions on SL(2,F_3) images of closed recognition walks) cites this. It is a one-line field projection, not a derived identity.
Claim. For a $2\times 2$ matrix $X=\begin{pmatrix}a&b\\c&d\end{pmatrix}$ with entries in $\mathbb{Z}/3\mathbb{Z}$, define $\operatorname{tr}(X):=a+d\in\mathbb{Z}/3\mathbb{Z}$.
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 are the content; the module supplies a total well-formedness checker and a computable invariant blind to those two non-content operations.
Matrices here are the hand-rolled four-component structure Mat over $\mathbb{Z}/3\mathbb{Z}$ (fields $a,b,c,d$), not Mathlib Matrix, so that later kernel evaluation of thousands of products stays cheap. The invariant reads images in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$; the module header stresses that trace is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step.
Loop traces alone fail to separate the intended witness (they collide on two of the forty-eight automorphism images), so the full invariant also records traces of pairwise commutators. The present definition is only the raw diagonal sum used by those higher constructions.
proof idea
Pure definition: project the four-tuple to the sum of its diagonal components in $\mathbb{Z}/3\mathbb{Z}$. No lemmas, no tactics, no reduction.
why it matters
This is the atomic scalar the Loom invariant is built from. Same-module consumers include the adjugate determinant identity; outside, Cost.SymplecticAction uses the analogous 2×2 trace in Cayley–Hamilton form (B + adj B = (tr B)·I and the identity tr(AB)+tr(A·adj B)=(tr A)(tr B)), which underpins the σ-conservation ↔ area-preservation equivalence for ledger maps.
Further downstream hits appear in the multi-coordinate cost-Hessian operator (eigenvalue read as a trace) and in Regge hinge analysis (coordinate-permuted absolute triples and zero-mode coefficient algebra). In the framework map this sits under the Loom certificate layer for closed walks on the eight-tick octave (T7), not under the J-uniqueness or mass-ladder steps themselves.
It does not close any open scaffold: it is infrastructure the conjugation-blind invariant and the det/adjugate lemmas quote by name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.