countTrue_cons_false
plain-language theorem explainer
Prepending a false bit to a boolean word leaves the true-count unchanged. Anyone tracking symbol counts under the Fibonacci substitution cites this when peeling constructors. The proof is a one-line simp unfolding of the recursive true-count.
Claim. For every finite word $w$ over $\{\mathsf{true},\mathsf{false}\}$, the number of $\mathsf{true}$ symbols in $\mathsf{false}::w$ equals the number of $\mathsf{true}$ symbols in $w$.
background
The module studies a two-letter substitution system whose symbol counts obey Fibonacci recurrences. Locally a word is a finite list of booleans; the true-count is the recursive tally that returns $0$ on the empty list and adds $1$ precisely when the head is true.
The companion false-count and the four cons lemmas (true/false head for each counter) form the elementary arithmetic layer. Upstream, the true-count is defined by cases on the list constructor, so the false-head case is immediate from that definition.
proof idea
One-line wrapper: simp [countTrue] unfolds the recursive definition on a cons cell whose head is false, so the indicator contributes $0$ and the equality reduces to reflexivity on the tail count.
why it matters
Feeds the induction step of counts_sub_word, which states that under the Fibonacci substitution the false-count of the image equals the sum of both counts of the original word, while the true-count of the image equals the original false-count. Those additive identities are the bridge from the substitution rule to Fibonacci recurrences on counts, the module's stated purpose in the verification/necessity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.