invariantOf
plain-language theorem explainer
Computable fingerprint of a list of matrices in SL(2, Z/3Z): the sorted single-loop traces paired with the sorted traces of all pairwise commutators. Certificate readers and soundness proofs cite it as the depth-one-plus-depth-two reading of a closed-walk configuration. The body is a direct pair of sorted maps; no proof content.
Claim. For a finite list $M_s$ of matrices over $\mathbb{Z}/3\mathbb{Z}$, return the ordered pair $\bigl(\mathrm{sort}(\mathrm{tr}\,M_s),\,\mathrm{sort}(\mathrm{tr}\,[M_i,M_j]_{i<j})\bigr)$, where traces are lifted to natural numbers and the pairwise commutators are taken in list index order.
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 five; a finished utterance is a finite list of such words sharing one basepoint. Content is defined by two refusals: free reduction (spelling is not content) and simultaneous conjugation of every loop (basepoint is not content).
Matrices here are explicit $2\times 2$ components over $\mathbb{Z}/3\mathbb{Z}$, chosen so kernel products reduce cheaply. The scalar trN lifts the ring trace to a natural number so invariants are lists of Nat. Pairwise commutator traces (pairTraces) walk index pairs in fixed order and record $\mathrm{tr}[M,N]$; both sides of every later equality build that list the same way, so no permutation bookkeeping is needed on the depth-two half. A hand-rolled insertion sort (sortNat) freezes the multiset reading against library renames.
The module supplies a total well-formedness checker, this computable invariant, and theorems that the invariant is blind exactly to the two non-content operations. It carries no model and no search.
proof idea
Pure definition: map each matrix to its natural-number trace, sort that list; compute the fixed-order list of pairwise-commutator traces, sort that list; return the pair. No lemmas, no tactics.
why it matters
This is the raw fingerprint that invariant applies after evaluating a configuration against a multiplication table. Three soundness theorems sit directly on it: permutation invariance (an utterance is a multiset of loops; ordering is not content), simultaneous conjugation invariance (THE SOUNDNESS THEOREM: moving the common basepoint leaves the pair alone, because trace is a class function and commutator traces transform accordingly under det-one conjugation), and simultaneous adjugate invariance (time reversal costs nothing in the det-one subgroup, since no trace sees an adjugate).
In the Recognition setting the depth-one half is what an amplitude-style (abelianised) reading can see; the depth-two half is exactly the lower-central-series data that abelianisation destroys. Loop traces alone collide on two of the forty-eight automorphism images of the intended witness, so the commutator layer is load-bearing. The construction realises the module promise: a trusted checker for finished objects the kernel did not build, on the free group of rank five forced by the eight-tick window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.