fibSubWord
plain-language theorem explainer
Extends the single-symbol Fibonacci substitution to whole Boolean words by concatenating letter images. Anyone proving count recurrences or iterating the substitution cites this map. It is a one-line definition: list flatMap of the letter rule.
Claim. Let a word $w$ be a finite list over $\{\mathsf{false},\mathsf{true}\}$. The substituted word is the concatenation of the Fibonacci images of its letters, where $\mathsf{false}\mapsto[\mathsf{false},\mathsf{true}]$ and $\mathsf{true}\mapsto[\mathsf{false}]$.
background
The module studies a two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is a finite list of Booleans. The letter map sends false to the block [false, true] and true to the singleton [false].
That letter map is the classical Fibonacci (or rabbit) substitution. Extending it to words by concatenation is the standard free monoid morphism induced by the letter rule; the definition packages that morphism as a single operator on lists.
proof idea
Pure definition, not a proof. The body is the list operation flatMap applied to the letter substitution: each Boolean is replaced by its image block and the blocks are concatenated in order. No lemmas are invoked.
why it matters
This morphism is the engine of the Fibonacci iteration. The iterate starting from the seed [false] is defined by repeated application of the word map. The additive count lemma for substituted words decomposes false/true counts under one application, and the successor count identity for iterates unfolds the next iterate as the image of the previous word under this map, yielding the Fibonacci recurrence on counts. In the verification/necessity layer it supplies the combinatorial skeleton that forces Fibonacci growth of symbol counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.