iter
plain-language theorem explainer
The n-fold iterate of the Fibonacci letter substitution, started from the seed word of a single false bit. Count lemmas and the FibSubst certificate cite this orbit as the canonical sequence whose false/true tallies recover Fibonacci numbers. Defined directly by Mathlib function iteration of the word-level substitution map.
Claim. For each natural number $n$, write $\mathrm{iter}(n)$ for the Boolean word obtained by applying the Fibonacci substitution map $n$ times to the seed word $[\mathsf{false}]$.
background
The module develops a two-letter substitution system on Boolean words whose symbol counts obey Fibonacci recurrences. Locally, a word is a finite list of Booleans. The elementary rule fibSub rewrites each letter to a short block; fibSubWord extends that rule to whole words by concatenation (flatMap).
The object here is the discrete dynamical orbit of the seed [false] under that word map. (The imported Loom Word is a different type: lists of integers as closed walks. The FibSubst Word is List Bool.)
proof idea
One-line definitional wrapper: (fibSubWord^[n]) [false], i.e. Mathlib Function.iterate applied n times to the singleton seed. No proof obligations.
why it matters
Supplies the orbit used by counts_iter_succ (one-step count recurrence) and counts_iter_fib (false/true counts equal consecutive Fibonacci numbers). Those lemmas feed FibSubstCert, whose verification predicate states that Fibonacci counts emerge from substitution iteration. In the Recognition verification layer this is the concrete combinatorial generator behind necessity claims that Fibonacci structure is forced by the substitution, not inserted by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.