countFalse_cons_true
plain-language theorem explainer
Prepending a true bit to a boolean word leaves the false-count unchanged. Citation target for anyone inducting on Fibonacci substitution words when tracking symbol counts. The proof is a one-line simp unfolding of the recursive count definition.
Claim. For every finite boolean word $w$, the number of $\mathrm{false}$ symbols in $\mathrm{true}\mathbin{::}w$ equals the number of $\mathrm{false}$ symbols in $w$.
background
The module studies a two-letter substitution system on boolean words whose symbol counts obey Fibonacci recurrences. Here a word is simply a finite list of booleans.
The false-count is the recursive tally that returns $0$ on the empty word and, on a cons cell, adds $1$ exactly when the head is false, then continues on the tail. The companion true-count is defined symmetrically. These two tallies are the raw data that later lemmas relate under Fibonacci substitution.
Upstream, the count definition is the only nontrivial dependency; the word type is a local abbreviation of List Bool (distinct from the Loom walk-word type).
proof idea
One-line wrapper: simp [countFalse] unfolds the recursive clause on true :: w. The head is not false, so the indicator contributes $0$ and the equality reduces to reflexivity on the recursive call.
why it matters
Feeds the induction step of counts_sub_word, which states that false- and true-counts of a Fibonacci-substituted word decompose additively: the new false-count equals the sum of the old counts, and the new true-count equals the old false-count. That additive law is the bridge from the two-letter substitution to Fibonacci recurrences on counts, the module's stated purpose inside the verification/necessity layer. Without the true-cons simplification (and its false-cons sibling), the cons case of the induction does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.