Word
plain-language theorem explainer
A closed recognition walk, up to homotopy, is encoded as a finite word in five signed generators of the free group of rank five on the eight-state window. Anyone working with Loom certificates, free reduction, conjugation, or SL(2,Z/3Z) evaluation cites this type. It is a one-line type synonym for lists of integers, with no proof content.
Claim. A closed walk up to homotopy is a word $w$ in the free group of rank five on the signed cotree generators: formally $w \in \mathrm{List}(\mathbb{Z})$, where nonzero entries are the generators $\pm 1,\ldots,\pm 5$.
background
On the eight-state, three-axis window fixed by the forcing chain (T7 eight-tick octave, T8 $D=3$), closed recognition walks up to homotopy form a free group of rank $E-V+1=5$. A finished recognition history is therefore a word in five signed generators.
The Loom module is a certificate language for configurations of such closed walks. Spelling is not content, so words are later read up to free reduction; basepoint choice is not content either, handled by simultaneous conjugation. The type itself only names the raw carrier: finite lists of integers standing for generator indices with sign.
Upstream, related "closed" predicates on plaquettes and dominos record ledger parity (zero-sum faces). A sibling Fibonacci-substitution Word is lists of booleans and is unrelated; here the integers index the five cotree generators.
proof idea
Pure abbreviation: Word is definitionally List Int. No lemmas, tactics, or reduction steps. Downstream code treats nonzero list entries as signed generators $\pm 1,\ldots,\pm 5$ and builds free reduction, inversion, and conjugation on top of this carrier.
why it matters
This is the atomic carrier for the entire Loom stack. Config is a list of such words (an utterance at one basepoint). Free reduction (consRed, reduceWord), inversion, conjugation (conjWord), abelianisation (abel), and matrix evaluation (evalWord, det_evalWord) all take Word as input.
Certificate data such as autSubst records the action of the forty-eight window automorphisms as lists of words in these generators. The module's invariant (traces and commutator traces in $\mathrm{SL}(2,\mathbb{Z}/3\mathbb{Z})$) is blind exactly to free reduction and simultaneous conjugation; without a uniform word type those theorems have no domain.
In the Recognition framework this sits under the eight-tick, rank-five free group picture of closed walks, not under mass ladders or $\alpha$ numerics. It carries no model and no search: only the type of finished objects the checker and invariant will accept.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.