Word
plain-language theorem explainer
Binary words are finite lists of booleans, the carrier type for a two-letter substitution system. Anyone working the Fibonacci-count lemmas in this module cites it as the ambient alphabet. The declaration is a one-line type synonym for List Bool, with no proof content.
Claim. A word is a finite sequence of letters from a two-letter alphabet $\{0,1\}$, represented as a list of booleans.
background
The module studies a two-letter substitution system whose letter counts obey Fibonacci recurrences. The alphabet is Boolean: false and true stand for the two generators. Words are ordinary finite lists over that alphabet.
Sibling definitions build the Fibonacci sequence, the substitution map on letters and on words, and the counters of false and true letters. Those counters are the objects that later satisfy the Fibonacci identities.
An identically named Word exists in the Loom core as lists of signed integers (closed walks in five generators). That is a different type; the present synonym is strictly Boolean and local to the Fibonacci-substitution verification path.
proof idea
Pure definitional abbreviation: Word is definitionally equal to List Bool. No tactics, no lemmas, no reduction steps.
why it matters
This type is the ambient carrier for the whole FibSubst development: substitution on words, false/true counts, and the Fibonacci recurrences those counts satisfy. Downstream consumers include the substitution action data and the free-reduction and evaluation machinery that read words, as well as configuration and conjugation helpers that thread word lists. In the Recognition verification stack it supplies the combinatorial substrate for necessity arguments that track Fibonacci growth, rather than a physical law itself. It does not touch the forcing chain T0–T8 or the J-cost directly; it sits under the verification/necessity layer that certifies combinatorial side conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.