evalWord_substWord
plain-language theorem explainer
Evaluating a generator word after a window automorphism acts on its letters equals evaluating the original word under the pushed-forward matrix table. Anyone proving that the Loom configuration invariant is blind to the forty-eight automorphisms of the eight-state window cites this identity. The proof is a short induction on the word, reducing the cons case via append and single-letter substitution.
Claim. Let $T$ be a table sending each of the five signed generators to a pair of matrices in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, let $\sigma$ be a substitution of generators by words (an automorphism of the recognition window), and let $w$ be a word. Then evaluating the substituted word under $T$ equals evaluating $w$ under the table obtained by applying $\sigma$ to $T$: $\mathrm{eval}_T(\sigma\cdot w)=\mathrm{eval}_{T\circ\sigma}(w)$.
background
Loom is a certificate language for finished recognition histories on the eight-state, three-axis window forced by the T0–T8 chain (in particular T7's eight-tick octave). Closed walks up to homotopy form a free group of rank five, so a finished utterance is a finite list of words in five signed generators sharing one basepoint. Content ignores free reduction and simultaneous conjugation; the module supplies a total well-formedness checker and a computable invariant blind to exactly those operations.
A table assigns to each generator the matrix image of the letter and of its inverse. A substitution is the data of an automorphism of the window: each generator is sent to a word. Word evaluation is the structural product of letter matrices, with the empty word mapping to the identity; appending therefore admits an easy induction.
The invariant reads traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ of loop images and of their pairwise commutators (depth-two lower-central data). Trace is a class function, so conjugation-blindness is a ring identity rather than a canonicalisation step.
proof idea
Induction on the word $w$. The empty word is immediate (both sides are the identity). In the cons case, rewrite the substituted word as the concatenation of the image of the head letter with the substituted tail; apply the append law for evaluation; invoke the inductive hypothesis on the tail; reduce the head via the single-letter substitution lemma; and finish with the cons clause of evaluation. No external arithmetic is required beyond the structural lemmas already in the module.
why it matters
This is the word-level engine behind the relabelling half of Loom soundness. Downstream, invariant_substConfig lifts the identity to whole configurations: reading a relabelled utterance is reading the original under the relabelled homomorphism, so the forty-eight automorphisms of the window are checked by forty-eight tables and no word is rewritten. That is exactly the quotient the module header ties to vertex homogeneity and to the refusal to let observables depend on supplied labels. Without the present lemma, the invariant could not be shown blind to window automorphisms while remaining a pure table-and-trace computation. It sits inside the Loom certificate layer rather than the forcing chain itself, but it makes the T7 eight-state window's automorphism group operational for finished certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.