invariant_map_invWord
plain-language theorem explainer
Reversing every closed walk in an utterance leaves the Loom invariant unchanged. Certificate readers checking orientation or gauge blindness cite this equality. The proof pushes evaluation through matrix adjunction wordwise, then applies the identity that the invariant is blind to adjunction.
Claim. Let $T$ be a well-formed generator table (each generator paired with its matrix image and inverse image) and let $c$ be a configuration: a finite list of closed walks sharing one basepoint. Replacing every walk by its free-group inverse leaves the Loom invariant of $c$ unchanged: $\mathrm{inv}(T, c^{\mathrm{inv}}) = \mathrm{inv}(T, c)$.
background
Loom is a certificate language for finished recognition histories on the eight-state, three-axis window. A closed history is a word in the free group of rank five; an utterance (configuration) is a finite list of such words at one basepoint. Content ignores free reduction and simultaneous conjugation; the module supplies a total well-formedness checker and a computable invariant blind exactly to those operations.
The invariant evaluates each reduced word in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ via a table $T$ that sends each generator to a matrix pair (image, inverse image), then reads ordinary traces together with traces of pairwise commutators (depth-two lower-central data). Trace is a class function, so conjugation blindness is algebraic rather than a canonicalisation step.
Here $\mathrm{invWord}$ reverses a single loop (free-group inverse). The claim is the simultaneous version: map every loop of the utterance by that inverse and the invariant stays put.
proof idea
Two steps. First, evaluation of the inverted configuration equals the original evaluation with each matrix replaced by its adjoint: $\mathrm{evalConfig},T,(c.\mathrm{map},\mathrm{invWord}) = (\mathrm{evalConfig},T,c).\mathrm{map},\mathrm{Mat.adj}$. This is List.map fusion plus the wordwise lemma that evaluating an inverted word under a well-formed table yields the adjoint of the original matrix image.
Second, unfold the invariant and apply the identity that the scalar invariant extracted from a list of matrices is unchanged when every matrix is replaced by its adjoint. The two facts cancel the map, giving equality on $c$.
why it matters
This is one half of the orientation/relabelling blindness package for Loom certificates: reversing every loop at once is not content. Downstream, invariant_gaugeImage in Loom.Separation rewrites gauge images through reduction, conjugation, and substitution; the flip branch needs exactly this inverse-map equality so that orientation reversal does not change the certificate value. The sibling abelian reading abelBag sits at depth one and deliberately loses the commutator data this invariant keeps; the present lemma shows the full invariant, not merely the abelian shadow, is stable under global inversion.
In the module narrative this pairs with conjugation blindness: spelling and basepoint are already quotiented, and global loop reversal is the remaining free-group automorphism that must not create fake distinctions. It sits on the eight-tick window (forcing T7) where closed walks form the rank-five free group the Loom language certifies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.