invWord
plain-language theorem explainer
Defines free-group inversion on Loom words: reverse the generator list and flip every sign. Anyone proving conjugation invariance, matrix evaluation of inverses, or that the configuration invariant is blind to simultaneous loop reversal cites this. The body is a one-clause recursive definition on lists.
Claim. For a word $w$ (a finite list of signed cotree generators, i.e. a closed walk up to homotopy), the inverse word is obtained by reversing the list and negating each entry: $\mathrm{inv}([])=[]$ and $\mathrm{inv}(x::t)=\mathrm{inv}(t)\mathbin{+\!+}[-x]$.
background
Loom treats finished recognition histories as configurations of closed walks on the eight-state, three-axis window fixed by the forcing chain. Up to homotopy those walks form a free group of rank five, so each loop is a word in five signed generators and an utterance is a finite list of such words sharing one basepoint.
A Word is simply List Int. Free reduction removes spelling as content; simultaneous conjugation of every loop removes basepoint choice as content. The module supplies a total well-formedness checker, a computable invariant valued in traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and theorems that the invariant is blind exactly to those two non-content operations.
Inversion of a single loop is the free-group inverse. Per loop it encodes denial (a content operation); applied uniformly to every loop it is a gauge move, which the invariant must ignore.
proof idea
Pure structural recursion on the list: the empty word inverts to empty; a cons cell inverts the tail and appends the negated head. No lemmas are invoked. The companion equation invWord_cons is definitional (rfl).
why it matters
Inversion is the algebraic half of basepoint change. Downstream, conjWord g w is defined as the free reduction of $g\mathbin{+!+}w\mathbin{+!+}\mathrm{inv}(g)$, so every conjugation identity routes through this definition. evalWord_invWord shows that evaluation in an admissible generator table sends the inverse word to the matrix adjugate, which is how $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ traces stay class functions. invariant_map_invWord then lifts that identity to configurations: reversing every loop at once leaves the Loom invariant unchanged, discharging the gauge half of the module's blindness claim. Substitution tables (tableOfSubst, ok_tableOfSubst, matAt_tableOfSubst) store both a word and its inverse image, so well-formedness of substituted tables also depends on this map. In the broader RS picture this sits under the eight-tick window and free-group rank $E-V+1=5$ from the forcing chain, not under mass or coupling numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.