pairTraces
plain-language theorem explainer
Ordered list of natural traces of pairwise commutators of a list of 2×2 matrices over Z/3Z. Supplies the depth-two half of the Loom configuration invariant, the part an abelianised (amplitude-style) reading destroys. Defined by a left-to-right recursion: each head is paired with every later matrix, the commutator trace is taken, and the results are concatenated. Downstream soundness proofs reuse this fixed order, so multiset reasoning appears only in the separate permutation lemma.
Claim. For a finite list $M_1,\ldots,M_n$ of $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$, return the concatenated list of natural traces $\mathrm{tr}([M_i,M_j])$ for all ordered pairs with $i<j$, walking left to right: each head against its tail, then recurse on the tail. The empty list yields the empty list.
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 homotopy form a free group of rank five, so a finished utterance is a finite list of words in five signed generators sharing one basepoint. Content is read up to free reduction and up to simultaneous conjugation (basepoint move); the module supplies a total well-formedness checker and a computable invariant blind exactly to those two non-content operations.
Matrices here are explicit $2\times 2$ structures over $\mathbb{Z}/3\mathbb{Z}$ (components rather than Matrix, for cheap kernel reduction). The invariant lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. Trace is a class function, so conjugation blindness is a ring identity. Loop traces alone collide on some of the forty-eight automorphism images of the intended witness, so the invariant also records traces of pairwise commutators: the depth-two data of the lower central series, exactly what abelianisation erases.
This definition builds that depth-two list in a fixed index order. Every theorem that compares two sides builds both lists the same way, so ordinary list equality suffices until a genuine reordering appears.
proof idea
Pure structural recursion on the input list, no lemmas. The empty case returns []. The cons case maps the tail with the function sending each later matrix $N$ to the natural trace of the commutator of the head with $N$, then appends the recursive call on the tail. The result is exactly the ordered family of pairwise commutator traces for index pairs $i<j$.
why it matters
This is the depth-two leg of invariantOf, which pairs sorted loop traces with sorted pairwise-commutator traces: "the first component is what an amplitude style reading can see and the second is what it cannot." Parent results that consume it are the soundness theorems invariantOf_cj (simultaneous conjugation by any determinant-one matrix leaves the invariant alone: "there is no first word") and invariantOf_adj (global inversion/adjugation is invisible, so time reversal in the gauge group costs nothing), plus pairTraces_perm, which lifts list permutation of the loops to multiset equality of the commutator-trace list (the swap case spends commutator-trace symmetry).
In the Recognition framework this sits inside the Loom certificate layer for closed walks on the eight-tick octave window (T7), where the free-group rank is $E-V+1=5$. Depth-two commutator data is what separates configurations that pure abelian (trace-of-loops) readings cannot. The module carries no model and no search: it only certifies finished objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.