counts_sub_false
plain-language theorem explainer
Substituting the single symbol false under the Fibonacci morphism yields a word with exactly one false and one true. Anyone tracking Boolean-word counts through the Fib substitution cites this base case. The proof is a one-line simp unfolding of the substitution rule.
Claim. Under the Fibonacci substitution sending $\mathrm{false}\mapsto[\mathrm{false},\mathrm{true}]$ and $\mathrm{true}\mapsto[\mathrm{false}]$, the image of $\mathrm{false}$ contains exactly one $\mathrm{false}$ and one $\mathrm{true}$.
background
The module studies a two-letter substitution system on Boolean words that produces Fibonacci recurrences for symbol counts. A word is a list of Booleans. The single-symbol Fibonacci substitution maps false to the length-two word [false, true] and true to the singleton [false]. Counts of false and true symbols are the obvious recursive tallies along a word.
This lemma records the count pair on the image of the single symbol false. It is the false half of the base data needed before extending counts from symbols to full words by concatenation.
proof idea
One-line wrapper: simp [fibSub] unfolds the substitution clause for false to the concrete word [false, true], after which the recursive count definitions evaluate to 1 and 1.
why it matters
Feeds the inductive step of counts_sub_word, which states that counts on a fully substituted word decompose as countFalse(fibSubWord w) = countFalse w + countTrue w and countTrue(fibSubWord w) = countFalse w. That additive law is the combinatorial engine of the Fibonacci recurrence for this substitution system, used in the Verification.Necessity layer to force Fibonacci growth of recognition counts. It is local bookkeeping, not a forcing-chain landmark, but it closes the false base case of the count morphism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.