evalWord_conjWord
plain-language theorem explainer
Evaluating a conjugated loop word equals conjugating its matrix image: the image of g w g^{-1} is the conjugate of the image of w by the image of g, for any well-formed generator table. Cited by anyone proving basepoint-independence of the Loom configuration invariant or conjugation-blindness of loop traces. Proof is a short simplification unfolding word conjugation and applying the evaluation lemmas for reduction, append, and inverse.
Claim. Let $T$ be a well-formed generator table (each generator mapped to a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$). For words $g,w$ in the five signed cotree generators, evaluation intertwines free-group conjugation with matrix conjugation: $\mathrm{eval}_T(gwg^{-1}) = \mathrm{eval}_T(g)\,\mathrm{eval}_T(w)\,\mathrm{eval}_T(g)^{-1}$.
background
The Loom module is a certificate language for 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 each loop is a word in five signed generators, and an utterance is a finite list of such words sharing one basepoint. Spelling is not content (free reduction), and basepoint choice is not content (simultaneous conjugation of every loop).
A table assigns to each generator a matrix and its inverse in component form over $\mathbb{Z}/3\mathbb{Z}$. Word evaluation multiplies those matrices along the letters. Word conjugation builds the free-group conjugate $gwg^{-1}$ (then reduces); matrix conjugation is $ABA^{-1}$. The doc-comment states the geometric reading: moving one loop's basepoint is conjugating its image.
Upstream evaluation lemmas already say that, under a well-formed table, evaluation respects free reduction, concatenation, and inversion. This theorem is the conjugation case of that homomorphism property.
proof idea
Term proof by targeted simplification. Unfold the definition of word conjugation (concatenate $g$, $w$, and the inverse word of $g$, then reduce). Rewrite with the lemmas that evaluation respects free reduction under a well-formed table, that evaluation of a concatenated word is the product of the evaluations, and that evaluation of an inverse word is the matrix inverse. Match the unfolded definition of matrix conjugation and finish with associativity of matrix multiplication. No case split and no induction.
why it matters
Feeds two parent results in the same module. The first is the depth-one nesting lemma: normalized trace of a conjugated word equals the original trace, because trace is a class function once evaluation intertwines conjugations; the doc-comment there notes this is exactly why the invariant must also read commutators. The second is the joint soundness fact that respelling every loop and moving the shared basepoint leave the configuration invariant alone, obtained by mapping the evaluation identity across the whole utterance.
In the Loom story this is the algebraic half of basepoint-independence. Closure already forces conjugation by prefixes of a closed walk (a map from a circle names no preferred vertex). The step from prefixes to arbitrary conjugators is the same refusal to let an observable depend on a supplied label that motivates quotienting by the 48 automorphisms of the window. Without this intertwining, the invariant could not be certified blind to the two declared non-content operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.