invariant
plain-language theorem explainer
The Loom invariant assigns to a generator table and a configuration the pair of sorted natural-number lists obtained by evaluating the loops in SL(2, Z/3Z) and reading both loop traces and pairwise-commutator traces. Certificate authors cite it as the content fingerprint of a finished utterance of closed recognition walks. The definition is a one-line wrapper: evaluate the config, then pass the image to the multiset reader invariantOf.
Claim. For a generator table $T$ (each generator mapped to a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ for the generator and its inverse) and a configuration $c$ (a finite list of closed words sharing one basepoint), the invariant is the pair of lists of natural numbers $\mathrm{invariantOf}(\mathrm{evalConfig}(T,c))$, i.e. the sorted multiset of loop traces together with the sorted multiset of pairwise-commutator traces of the evaluated loops.
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 $E-V+1=5$, so an utterance is a finite list of words in five signed generators at a common basepoint. Content is defined by two refusals: spelling is not content (free reduction), and choice of basepoint is not content (simultaneous conjugation of every loop).
A Table assigns to each generator the pair of matrices (image and inverse image) in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$. A Config is simply a list of words. Trace is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step. Loop traces alone collide on some automorphism images, so the invariant also records traces of pairwise commutators (depth-two lower-central-series data), which abelianisation destroys.
The module supplies a total well-formedness checker, this computable invariant, and the theorems that the invariant is blind exactly to free reduction and simultaneous conjugation. It carries no model and no search.
proof idea
One-line definitional wrapper. Evaluate the configuration under the table via evalConfig, then hand the resulting matrix data to invariantOf, which reads the multiset of loop traces and the multiset of pairwise-commutator traces and returns them as a pair of sorted List Nat. The adjacent comment records that the sort is honest: the invariant sees a multiset, not an ordered list. No tactic proof; the body is pure composition.
why it matters
This is the content fingerprint of the Loom certificate layer. Downstream, the module's invariance theorems show it is unchanged under free reduction and under simultaneous conjugation, so two utterances that differ only by non-content operations share the same pair of lists. That matches the module claim that a finished history is a map from a circle and names no preferred vertex.
In the broader Recognition framework it sits on the eight-tick octave and the free-group structure of closed walks on the forced window (T7, rank-five generators). Trace-plus-commutator data in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ is the concrete separator used when loop traces alone fail on the 48 window automorphisms. Used-by edges reach Action/Noether flows, cost-algebra normalisations, and alpha-derivation bookkeeping, where a stable configuration label is needed. It closes no open scaffold itself; it is the definition those blindness theorems quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.