invariantOf_perm
plain-language theorem explainer
Permutation of a list of loop matrices leaves the Loom invariant unchanged: both the sorted traces and the sorted pairwise-commutator traces are multiset data. Anyone proving that utterance order is non-content cites this. The proof is a two-line simp that rewrites the invariant definition through the already-proved permutation lemmas for sorted Nats and for pairTraces.
Claim. If $M_s$ and $N_s$ are lists of matrices over $\mathbb{Z}/3\mathbb{Z}$ that are permutations of each other, then $\mathrm{invariantOf}(M_s)=\mathrm{invariantOf}(N_s)$, i.e. the sorted list of traces and the sorted list of pairwise commutator traces agree.
background
The Loom module is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window fixed by the forcing chain (T7 eight-tick octave, T8 $D=3$). A finished utterance is a finite list of words in the free group of rank five; content is what survives free reduction and simultaneous conjugation.
Mat is the componentwise stand-in for $2\times 2$ matrices over $\mathbb{Z}/3\mathbb{Z}$ (used instead of Matrix for cheap kernel evaluation). Trace is exported as a natural via trN so invariants are sortable lists of Nat. The invariant of a list of matrices is the pair
$(\mathrm{sortNat}(\mathrm{map},\mathrm{trN}, M_s),,\mathrm{sortNat}(\mathrm{pairTraces}, M_s))$
: depth-one traces together with depth-two pairwise commutator traces. Loop traces alone collide on automorphism images; commutator traces supply the missing separation.
Upstream, sortNat_eq_of_perm says sorting is a multiset quotient, and pairTraces_perm says pairwise commutator traces of a reordered list form the same multiset (the swap case spends commutator-trace symmetry).
proof idea
Term-mode via simp only. Unfold invariantOf to the pair of sorted lists. The first component becomes equal by sortNat_eq_of_perm applied to the image of the given permutation under List.map Mat.trN. The second component becomes equal by sortNat_eq_of_perm applied to pairTraces_perm h, which already supplies the permutation of the pairwise-commutator-trace lists. No further algebra is needed.
why it matters
This is the multiset half of Loom soundness: ordering of loops is not content. The module doc states the invariant must be blind to exactly the two non-content operations (spelling/reduction and basepoint/conjugation); this theorem discharges the ordering half at the matrix level.
It feeds invariant_perm, which lifts the same fact to configurations by mapping words through a table evaluation and then applying this result. It also appears in the axiom audit of abelBag (the depth-one abelianised reading). Together with the conjugation-blindness theorems, it makes the computable invariant a genuine certificate of utterance content rather than of presentation order. Framework-wise it sits inside the Loom certificate layer built on the free group of closed walks on the forced eight-tick window; it does not itself touch J-uniqueness, phi, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.