Subst
plain-language theorem explainer
A relabelling of the recognition window is a list of five words: the images of the signed cotree generators under an automorphism. Anyone checking that the Loom invariant is blind to the 48 window automorphisms cites this type. It is a one-line type alias for lists of free-group words.
Claim. A substitution (relabelling) is a finite list of words in the five signed cotree generators. Each entry is the image of one generator under an automorphism of the recognition window, so the list encodes how that automorphism acts on the free group of rank $5$.
background
The Loom module is a certificate language for configurations of closed recognition walks on the eight-state, three-axis window forced by the T0–T8 chain. Closed walks up to homotopy form a free group of rank $E-V+1=5$, so each loop is a word in five signed generators (a Word: a list of integers). An utterance is a finite list of such words sharing one basepoint.
Content is quotiented by free reduction and by simultaneous conjugation (basepoint change). The remaining discrete symmetry is the automorphism group of the window (order 48). An automorphism acts on generators by sending each to some reduced word; the data of that action is exactly a list of five words.
Upstream, Word is the free-group word type. The Fibonacci-side Word (lists of booleans) is a different alphabet and is not used here.
proof idea
One-line abbreviation: Subst is defined to be List Word. No proof obligations; the mathematical content lives in the consumers (getWord, substLetter, substWord, tableOfSubst, and the invariance theorems).
why it matters
This type is the carrier for window automorphisms inside Loom. Downstream, getWord projects the $n$-th generator image; substLetter/substWord push a substitution through a word; tableOfSubst rebuilds the $SL(2,\mathbb{Z}/3)$ table by evaluating those images. The key soundness facts are evalWord_substWord (reading a relabelled utterance under a homomorphism equals reading the original under the relabelled table) and invariant_substConfig (the configuration invariant is unchanged after relabelling, so the 48 automorphisms are checked by 48 tables without rewriting words). That is the relabelling half of Loom soundness, tied to the free-group presentation of closed walks on the eight-tick window ($T7$) in $D=3$ ($T8$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.