invWord_cons
plain-language theorem explainer
Unfolding identity for free-group inversion on generator words: inverting a word that starts with signed generator x is the same as inverting the tail and appending -x. Anyone proving that matrix evaluation turns word inversion into adjugation cites it. The proof is pure reflexivity against the recursive clause of the inverse-word definition.
Claim. For every integer $x$ and every word $t$ (a finite list of signed cotree generators), $\mathrm{inv}(x{::}t)=\mathrm{inv}(t)\mathbin{+\!+}[-x]$.
background
Loom treats a finished recognition history as a finite list of closed walks on the eight-state, three-axis window. Up to homotopy those walks form a free group of rank five, so each loop is a word: a List Int of signed generators.
The operation that reverses a walk and negates every letter is the group-theoretic inverse. The module documents it as content when applied to a single loop (denial) and as gauge when applied simultaneously to every loop of an utterance. Its recursive definition on the empty list is empty, and on a cons cell is exactly the right-hand side of this identity.
The surrounding theory evaluates words in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ via a generator table; trace (and commutator traces) supply the conjugation-blind certificate of a configuration.
proof idea
One-line wrapper: rfl. The statement is definitionally identical to the cons clause of invWord, so no rewriting or induction is required.
why it matters
The sole recorded consumer is evalWord_invWord, which proves by induction on the word that evaluating the inverse yields the matrix adjugate of the original evaluation. The inductive cons step rewrites with this identity, then uses append-multiplicativity and the singleton case.
That evaluation identity is part of Loom's claim that the computable $\mathrm{SL}(2,\mathbb{Z}/3)$ invariant is blind exactly to the two non-content operations (free reduction and simultaneous conjugation). Inversion itself is content per loop; the lemma is bookkeeping that lets the matrix semantics respect the free-group inverse. It sits inside the certificate layer of the eight-tick, rank-five free group forced by the T7/T8 window, not inside the forcing chain proper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.