substWord_cons
plain-language theorem explainer
Substitution of a window automorphism through a nonempty word is letter substitution concatenated with the tail substitution. Anyone proving homomorphism compatibility of relabellings cites this. The proof is pure definitional unfolding (rfl).
Claim. For any window automorphism $\sigma$ (a list of five generator images), any signed generator letter $x\in\mathbb{Z}$, and any word $t$, the substituted word on the cons cell equals the concatenation $\mathrm{substLetter}(\sigma,x)\,++\,\mathrm{substWord}(\sigma,t)$.
background
In the Loom certificate language, a closed recognition walk up to homotopy is a word in five signed cotree generators: Word is List Int. An utterance is a finite list of such words sharing one basepoint. The module supplies a total well-formedness checker and a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3)$, blind to free reduction and simultaneous conjugation.
An automorphism of the recognition window acts by sending each generator to a word. That data is a substitution $\sigma:\mathrm{Subst}:=\mathrm{List},\mathrm{Word}$. Letterwise action sends a positive index to the corresponding image word, a negative index to the inverse word, and zero to the empty word. Wordwise action folds that letter map by concatenation: empty stays empty, and a cons cell becomes letter image appended to the substituted tail.
This lemma records the cons clause of that fold as an equality usable under rewriting.
proof idea
One-line wrapper: the goal is definitionally identical to the recursive clause of substWord, so rfl closes it. No lemmas are applied.
why it matters
The parent theorem is evalWord_substWord: reading a relabelled utterance under a homomorphism equals reading the original under the relabelled table. Its inductive step rewrites with this cons identity, then evalWord_append, the inductive hypothesis, evalWord_substLetter, and evalWord_cons.
That parent is what lets the forty-eight automorphisms of the eight-tick, three-axis window be checked by changing the evaluation table rather than rewriting every certificate word. In the Loom setting this is the algebraic half of content-blindness: spelling and basepoint are not content, and substitution through automorphisms must commute with evaluation so the invariant stays a class function on configurations. The free-group rank $E-V+1=5$ and the eight-tick octave (T7) fix the generator set being relabelled; this lemma is the tiny list identity that makes the commutation proof go through by induction on word length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.