trN
plain-language theorem explainer
Natural-number lift of the matrix trace over Z/3Z, so Loom configuration invariants are plain Nat lists that sort under a fixed hand-rolled order. Anyone citing the certificate invariant or its conjugation/permutation blindness uses this projection. The body is a one-line extraction of the ZMod representative.
Claim. For a $2\times 2$ matrix $X$ with entries in $\mathbb{Z}/3\mathbb{Z}$, $\mathrm{tr}_N(X)$ is the unique natural number in $\{0,1,2\}$ equal to the ring trace $\mathrm{tr}(X)=X_{11}+X_{22}\in\mathbb{Z}/3\mathbb{Z}$.
background
Loom is a certificate language for closed recognition walks on the eight-state, three-axis window. 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 exactly to those two non-content operations.
Matrices are the component structure Mat (four entries in $\mathbb{Z}/3\mathbb{Z}$), chosen over library Matrix so thousands of kernel products reduce cheaply. The ring trace tr is $a+d$. Trace is a class function on the determinant-one subgroup, which is why conjugation blindness is a ring identity rather than a canonicalisation step.
The natural lift exists so that depth-one loop traces and depth-two commutator traces can be collected as List Nat and sorted by a comparison no library change can move.
proof idea
One-line definition: apply the ring trace, then take the canonical Nat representative of the resulting element of $\mathbb{Z}/3\mathbb{Z}$ via .val. No lemmas, no tactics.
why it matters
This projection is the scalar the whole Loom invariant is built from. invariantOf maps each loop matrix to its natural trace and pairs that sorted list with pairTraces (natural traces of pairwise commutators). The soundness theorems invariantOf_cj (basepoint move is simultaneous conjugation), invariantOf_perm (utterance is a multiset), and invariantOf_adj (global reversal is adjugate, invisible to every trace) all reduce componentwise through this lift. Supporting identities such as trN_comm_adj and trN_conjWord likewise state equality after the lift, so the certificate remains a pure list of naturals. In the Recognition setting this is the depth-one half of the lower-central data that separates automorphism images an abelianised reading would collide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.