countFalse_nil
plain-language theorem explainer
The empty Boolean word contributes zero false symbols under the standard recursive count. Anyone discharging base cases in Fibonacci-substitution count identities will cite this. The proof is pure definitional reflexivity on the empty-list clause of the count.
Claim. If $w$ is the empty list of Booleans, then the number of $\mathrm{false}$ entries in $w$ equals $0$.
background
The module studies a two-letter substitution system whose symbol counts obey Fibonacci recurrences. Locally, a word is just a finite list of Booleans (List Bool), not the Loom cotree word type.
The count of false symbols is defined by recursion on the list: the empty list contributes $0$, and a cons cell adds $1$ precisely when the head is false. The matching true-count is defined the same way. These two tallies are the raw data that later lemmas relate to Fibonacci numbers under the substitution rules.
proof idea
One-line definitional proof. Unfolding the empty-list clause of the false-count definition yields $0 = 0$, discharged by rfl. The @[simp] attribute makes the base case fire automatically in later rewrites.
why it matters
Base case for every inductive argument on false-counts in the Fibonacci substitution calculus. Sibling lemmas handle the true-count empty case and the four cons cases; together they give a complete simp normal form for symbol tallies on Boolean words. Downstream Fibonacci identities for substituted words rest on these count reductions, even though no direct used_by edge is recorded yet. In the broader Recognition verification stack this is bookkeeping infrastructure, not a forcing-chain step (T0–T8), but it keeps the substitution-count layer free of manual case splits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.