substWord
plain-language theorem explainer
Homomorphic extension of a generator relabelling from letters to full words in the free group on five signed cotree generators. Anyone checking that Loom invariants are blind to the 48 window automorphisms cites this map. The definition is the standard free monoid extension: replace each letter by its image word and concatenate.
Claim. Given a relabelling $\sigma$ (a list of five words, one image per positive generator) and a word $w$ in the signed generators, $\mathrm{subst}(\sigma,w)$ is the word obtained by replacing each letter of $w$ by its image under $\sigma$ (positive generators by the corresponding word, negative generators by the inverse word) and concatenating. The empty word maps to the empty word.
background
Loom treats finished recognition histories as configurations of closed walks on the eight-state, three-axis window forced by the T0–T8 chain. Up to homotopy those walks form a free group of rank $E-V+1=5$, so each loop is a word in five signed generators (Word as a list of integers). An utterance is a finite list of such words sharing a basepoint.
Content is quotiented by free reduction and by simultaneous conjugation (basepoint change). Automorphisms of the recognition window act by sending each generator to a word; that data is a relabelling $\sigma$ (Subst as a list of words). Letterwise action sends a positive index to the corresponding word and a negative index to its inverse word, and ignores zero.
The module supplies a total well-formedness checker, a computable invariant valued in traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$, and theorems that the invariant is blind to the two non-content operations. Relabelling of whole words is the free extension of the letter map, needed before one can push automorphisms through configurations or evaluation tables.
proof idea
Pure structural recursion on the word: the empty list maps to empty; a cons cell concatenates the letter image under the letterwise relabelling with the recursive image of the tail. No lemmas are invoked; the companion one-line theorem simply unfolds this clause by rfl.
why it matters
This is the word-level action of window automorphisms that Loom must be blind to. It feeds the configuration-level map (apply the word map to every loop) and the key intertwining theorem: evaluating a relabelled word under a homomorphism equals evaluating the original word under the relabelled table. That theorem is what lets the forty-eight automorphisms be checked by changing the evaluation table rather than rewriting every certificate word.
In the broader Recognition picture the eight-tick octave and $D=3$ fix the window whose automorphism group is being quotiented; the free rank-five presentation is the closed-walk group on that window. Without a total, computable substitution on words, the invariant's claimed blindness to spelling and labelling would not be executable on finished certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.