conjWord
plain-language theorem explainer
Conjugation of a closed walk by a word g: free-reduce the concatenation g, w, g-inverse. This is the algebraic form of moving the shared basepoint of an utterance. Anyone proving Loom soundness or gauge blindness cites it. The body is a one-line composition of append, walk-inverse, and free reduction.
Claim. For words $g$ and $w$ in the free group on five signed generators (each a list of integers), the conjugate of $w$ by $g$ is the free reduction of the concatenation $g \, w \, g^{-1}$, where $g^{-1}$ is the reversed walk with every generator sign flipped.
background
In Loom, a finished recognition history is a closed walk on the eight-state, three-axis window forced by the T0–T8 chain. Closed walks up to homotopy form a free group of rank $E-V+1=5$, so each loop is a word in five signed generators (Word as List Int). An utterance is a finite list of such words sharing one basepoint.
Two operations are declared non-content: free spelling (adjacent cancelling pairs) and simultaneous basepoint move. Free reduction (reduceWord) is the total linear normalizer for spelling. Walk inverse (invWord) reverses the list and negates each letter; per loop that encodes denial, while conjugating every loop by the same $g$ encodes a shared basepoint shift.
The module supplies a well-formedness checker, a computable invariant valued in traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and proofs that the invariant is blind exactly to those two non-content moves. Trace is a class function, so conjugation blindness is a ring identity rather than a canonicalization step.
proof idea
Pure definition, not a proof. The body is the standard free-group conjugate written as lists: concatenate $g$, then $w$, then invWord g, and pass the result through reduceWord so the output is freely reduced. No tactics; the mathematical content is exactly that composition.
why it matters
This is the primitive that turns the phenomenological claim "where the utterance started is not content" into an algebraic operation on configurations. Downstream, evalWord_conjWord shows evaluation in the $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ table sends this to matrix conjugation; trN_conjWord then gets depth-one trace invariance for free from the class-function identity; invariant_conjWord lifts both facts to whole utterances (respelling plus shared basepoint move leave the invariant fixed).
gaugeImage in Separation folds conjugation together with window automorphisms and global flip as the full gauge action. Grammar's weaveBody builds configurations that later sit under this action. In the module narrative, closure already gives conjugation by walk prefixes (rotate_is_conjugation); extending to arbitrary $g$ is the same label-blindness that motivates the 48-automorphism quotient of the window. The definition is the concrete carrier of that second non-content premise inside the certificate language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.