invariant_perm
plain-language theorem explainer
If two Loom configurations differ only by reordering their closed loops, they share the same invariant under any evaluation table. Separation proofs that treat reorderings as non-content cite this equality. The argument is a one-line reduction: push the list permutation through word evaluation and apply the already-proved permutation invariance of the multiset of matrix data.
Claim. For every evaluation table $T$ and configurations $c,d$ (finite lists of closed words sharing a basepoint), if $c$ is a list-permutation of $d$, then the Loom invariant of $c$ under $T$ equals the Loom invariant of $d$ under $T$.
background
Loom treats a finished recognition history as an utterance: a finite list of closed walks on the eight-state, three-axis window, written as words in the free group of rank five that the forcing chain supplies. A configuration is exactly that list of words, all sharing one basepoint.
Two operations are declared non-content: free reduction (spelling) and simultaneous conjugation of every loop by one word (basepoint choice). The module also treats the order of the loops in the list as non-content. The computable invariant evaluates each word in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ via a table of generator matrices, then records ordinary traces together with traces of pairwise commutators (depth-two lower-central data). Because the invariant is built from a multiset of those matrix quantities, it must be blind to list order.
An evaluation table assigns to each generator the pair of matrices for the generator and its inverse.
proof idea
Pure term proof, one application. The hypothesis is a list permutation $h : c \sim d$. Map $h$ through word evaluation under $T$ to obtain a permutation of the evaluated matrix lists, then invoke the upstream lemma that the underlying invariant-of-evaluated-words is unchanged by list permutation. No induction or case split appears at this layer.
why it matters
The two separation theorems in Loom.Separation rewrite along this lemma. Both no_gauge_image_of_A_is_B and no_gauge_image_of_C_is_D must show that no gauge image of one witness configuration can match another, where gauge includes automorphism relabelling, global loop reversal, basepoint move, respelling, and reordering. Each proof first absorbs a permutation hypothesis via this equality, then applies gauge-image invariance and reads a precomputed inequality from the separation table.
Without order-blindness the invariant would not be a function of unordered content, and those certificates would fail on harmless reorderings. In the broader Loom story this is the third blindness (after free reduction and conjugation) that makes the invariant a certificate of meaning rather than of spelling or presentation. It sits downstream of the free-group model of closed walks on the eight-tick window and upstream of the concrete A/B and C/D separation claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.