fibSub
plain-language theorem explainer
The classical Fibonacci substitution on one Boolean symbol: false maps to the block false-true, true maps to the singleton false. Anyone checking that iterated substitution produces Fibonacci letter counts cites this map as the generator. It is a pure case definition, not a theorem.
Claim. Define the Fibonacci substitution $\sigma$ on a single Boolean letter by $\sigma(\mathsf{false}) = [\mathsf{false},\mathsf{true}]$ and $\sigma(\mathsf{true}) = [\mathsf{false}]$, where words are finite lists of Booleans.
background
The module studies a two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is simply a finite list of Booleans. The classical Fibonacci substitution is the morphism that replaces each letter by a short block so that iterating the map on a seed word yields lengths and counts matching $F_n$.
In this file the alphabet is ${\mathsf{false},\mathsf{true}}$. The companion sequence $F$ is the usual Fibonacci sequence with $F(0)=0$, $F(1)=1$. Downstream, the same substitution is extended to whole words by concatenation (flatMap), and separate counters tally how many false and true symbols appear.
An upstream Loom notion of Word (lists of signed cotree generators) is unrelated; the local Word is purely Boolean.
proof idea
No proof. The declaration is a two-clause pattern match on Bool that returns the corresponding constant list. Downstream lemmas such as counts_sub_false and counts_sub_true simply unfold this definition with simp.
why it matters
This is the atomic generator for the Fibonacci-substitution verification stack. It is consumed by fibSubWord (extension to words by concatenation), by the count lemmas counts_sub_false, counts_sub_true and counts_sub_word (which show that one substitution step acts on counts by the Fibonacci matrix), and by the certificate structure FibSubstCert, whose predicate states that Fibonacci counts emerge from substitution iteration.
In the broader Recognition verification layer the construction supplies a concrete, machine-checked witness that a simple local rewrite rule forces global Fibonacci growth. That growth pattern is the combinatorial skeleton behind self-similar fixed-point structure (phi) elsewhere in the forcing chain, though this definition itself stays purely combinatorial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.