trN_conjWord
plain-language theorem explainer
Conjugation of a closed walk by any word leaves the normalized matrix trace unchanged. Loom users cite this when arguing that nesting (a binder around a loop) is invisible at depth one of the invariant. The proof rewrites evaluation of a conjugate as matrix conjugation, then applies the class-function identity for normalized trace on SL(2, Z/3Z).
Claim. Let $T$ be a well-formed generator table (each generator and its inverse map to matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$). For any words $g$ and $w$ in the five signed cotree generators, if $\mathrm{conj}(g,w)$ denotes the conjugate word $gwg^{-1}$, then the normalized trace of the matrix image of $\mathrm{conj}(g,w)$ equals the normalized trace of the matrix image of $w$.
background
Loom is a certificate language for finished 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 five, so each loop is a word in five signed generators, and an utterance is a finite list of such words sharing one basepoint.
Content is defined by two refusals: free reduction (spelling is not content) and simultaneous conjugation of every loop by one shared word (basepoint is not content). The module supplies a total well-formedness checker, a computable invariant valued in traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and theorems that the invariant is blind exactly to those two operations. Matrices are stored by components over $\mathbb{Z}/3\mathbb{Z}$ for cheap kernel evaluation; a table assigns to each generator its image and the image of its inverse.
Trace is a class function, so blindness to conjugation is a ring identity rather than a canonicalisation step. Loop traces alone do not separate the intended witness (they collide on two of the forty-eight automorphism images), which is why the invariant also reads pairwise commutator traces.
proof idea
Term-mode, two steps. First rewrite the evaluation of the conjugate word via the lemma that evaluating $\mathrm{conj}(g,w)$ under a well-formed table yields the matrix conjugate $A M A^{-1}$, where $A$ and $M$ are the images of $g$ and $w$. Then simplify the normalized-trace definition using the class-function identity: normalized trace is invariant under conjugation by any matrix of determinant one. The determinant-one hypothesis is discharged by the lemma that every evaluated word under a well-formed table lands in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$.
why it matters
This is the algebraic reason nesting is invisible at depth one. Downstream, the grammar theorem on quantified weave bodies uses it to show that every loop of a quantified body is a conjugate of the corresponding loop of the bare body, so the lists of loop traces agree pointwise; only commutators of the loops with each other move. That is exactly the measured fact that loop traces alone fail to separate the witness, and why the invariant must read depth-two lower-central-series data.
In the Loom header this closes the conjugation half of the non-content package: free reduction handles spelling; this theorem (with the basepoint-forced rotation argument) handles shared basepoint change. It sits inside the eight-tick, rank-five free-group picture of closed recognition walks, not in the mass or coupling ladder, but it is the certificate-side reason a finished utterance can be checked without depending on how binders were written.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.