getWord
plain-language theorem explainer
Indexes a generator substitution (a list of image words for the five cotree generators) by a natural number, returning the empty word when the index is out of range. Anyone applying a window automorphism to a letter or building the substituted matrix table cites this accessor. The body is plain structural recursion on the list and the index.
Claim. Given a substitution $\sigma$ (a finite list of words, one image per generator under a window automorphism) and an index $n\in\mathbb{N}$, return the $n$-th word of $\sigma$. If $\sigma$ is empty or $n$ exceeds its length, return the empty word.
background
In the Loom certificate language, a closed recognition walk up to homotopy is a word in five signed cotree generators (Word as a list of integers). An utterance is a finite list of such words sharing one basepoint. The free group of rank $E-V+1=5$ on the eight-state, three-axis window is the ambient algebra.
A substitution (Subst) packages how an automorphism of the recognition window acts on those generators: each generator is sent to a word, so a relabelling is simply a list of words. The module supplies a total well-formedness checker and a computable invariant in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$ that is blind to free reduction and simultaneous conjugation.
getWord is the zero-based lookup into that list. Downstream letter substitution and table evaluation both need a total way to read the image of generator $n$ without partiality.
proof idea
Definition by pattern matching, not a theorem. Empty substitution yields the empty word for every index. Head of a nonempty list is returned at index $0$. For successor indices the call recurses on the tail. No lemmas are invoked; totality follows from structural recursion on the list.
why it matters
This is the primitive read for applying window automorphisms inside Loom. substLetter uses it to replace a signed generator index by the corresponding image word (or its inverse). matAt_tableOfSubst uses it to evaluate the substituted generator table entrywise as a pair of matrix images under a fixed representation table.
Without a total index into the substitution list, the certificate language could not push automorphisms through words or compare invariants of relabelled configurations. It sits under the Loom claim that the invariant is blind exactly to free reduction and simultaneous conjugation, on the free group of rank five forced by the eight-tick window (T7) and $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.