pairTraces_perm
plain-language theorem explainer
Reordering a list of matrices leaves the multiset of pairwise commutator traces unchanged. Loom invariant soundness cites this as the multiset half: loop order is not content. Proof is induction on List.Perm; the swap case spends Mat.trN_comm_symm.
Claim. If $M_s$ and $N_s$ are finite lists of $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$ and $N_s$ is a permutation of $M_s$, then the list of pairwise commutator traces of $M_s$ is a permutation of that of $N_s$.
background
Loom certifies finished configurations of closed recognition walks on the eight-state, three-axis window. Closed walks up to homotopy are words in a free group of rank five; an utterance is a finite list of such loops sharing a basepoint. Content ignores free reduction and simultaneous conjugation; the module supplies a computable invariant blind to those operations.
Matrices are the structure Mat with four ZMod 3 entries (components rather than Matrix, for cheap kernel reduction). The invariant evaluates loop images in SL(2, ZMod 3) and, because plain traces collide on some automorphism images, also the traces of pairwise commutators (depth-two lower-central data). pairTraces builds that list of commutator traces from a list of matrices.
Trace is a class function, so conjugation blindness is algebraic. Multiset blindness to reordering the loops is a separate claim and is what this lemma isolates.
proof idea
Induction on the List.Perm hypothesis.
nil: reflexivity of permutation.cons: unfoldpairTraces, thenList.Perm.appendof the mapped head block with the inductive hypothesis.swap: unfoldpairTracesand the two-cons append shape; rewrite byMat.trN_comm_symm(commutator-trace symmetry in the two arguments) so the swapped pair produces the same head entries; finish withList.Perm.consandperm_append_left_comm.trans: compose the two inductive permutation witnesses.
The only non-structural ingredient is commutator-trace symmetry on the adjacent transposition.
why it matters
Feeds invariantOf_perm directly: that theorem is the multiset half of Loom soundness, stating that an utterance is read as a multiset of loops and that no ordering of the loops is content. Its proof sorts both the plain traces and the pairwise commutator traces, and the second sort equality is exactly pairTraces_perm.
In the Recognition setting this closes one of the two non-content operations the Loom header isolates (spelling/order versus basepoint conjugation). The eight-tick window and free-group rank five fix the ambient language; the invariant itself stays model-free and only checks finished objects. Without multiset invariance, the certificate would still depend on an arbitrary listing of loops, which the module explicitly refuses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.