substLetter
plain-language theorem explainer
A signed generator letter is sent through a window automorphism to a free-group word: positive indices pick the image word, negative indices take its free inverse, and zero yields the empty word. Anyone tracking Loom relabellings or free-group automorphisms of the five cotree generators cites this map. The body is a three-way case split on the sign of the integer letter, using list lookup and free inversion.
Claim. Given a substitution $\sigma$ (a finite list of words, one image per generator) and a signed letter $x\in\mathbb{Z}$, return the substituted word: if $x>0$, the $(|x|-1)$-st entry of $\sigma$; if $x<0$, the free inverse of that entry; if $x=0$, the empty word.
background
Loom treats a finished recognition history as a finite list of closed walks on the eight-state, three-axis window. Up to homotopy those walks form a free group of rank five, so each loop is a word in five signed generators (encoded as a list of nonzero integers). Spelling is not content: words are read up to free reduction. Basepoint is not content either: simultaneous conjugation of every loop is gauge.
A window automorphism acts on the five generators by sending each to a word. That data is a substitution: a list of five (or fewer) words. Looking up the $n$-th image word is ordinary list indexing with empty default past the end. Free inversion reverses the walk and negates every letter; applied to one loop it encodes denial, applied uniformly it is gauge.
The present map is the single-letter action of a substitution: it turns one signed generator index into the corresponding image word (or its inverse).
proof idea
Pure definition by cases on the sign of the integer letter. If $x>0$, return the $(|x|-1)$-st word of the substitution via list lookup. If $x<0$, return the free inverse of that same lookup. If $x=0$, return the empty list. No lemmas are invoked; the body is the three-branch conditional itself.
why it matters
This is the atomic step of the free-group automorphism action used throughout Loom. Extending letterwise by concatenation yields the full word substitution, and the cons equation for that extension is definitional. Downstream, the evaluation theorem states that substituting then reading the word in a matrix table equals reading the letter in the substituted table: the letter map intertwines substitution with the $\mathrm{SL}(2,\mathbb{Z}/3)$ representation that supplies Loom's conjugation-blind invariant (traces of loops and of their pairwise commutators).
In the Recognition setting the five generators are the free basis of closed walks forced by the eight-tick, three-axis window (T7, T8). Automorphisms of that window are exactly the relabellings the invariant must ignore; this letter map is how those relabellings act on words before the invariant is computed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.