countTrue_cons_true
plain-language theorem explainer
Prepending a true bit to a boolean word raises the true-count by exactly one. Citation target for anyone inducting on letter counts under the Fibonacci substitution. The proof is a one-line simp wrapper that unfolds the recursive count and normalizes Nat addition.
Claim. For every boolean word $w$, the number of true entries in the cons $\mathrm{true}::w$ equals the number of true entries in $w$ plus one: $\#_{\mathrm{true}}(\mathrm{true}::w)=\#_{\mathrm{true}}(w)+1$.
background
The module studies a two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is simply a list of booleans. The true-count is the recursive tally of entries equal to true (nil contributes zero; cons branches on the head bit).
Local lemmas of this shape (nil base cases and the four cons cases for true/false counts) equip induction over words. Downstream, the Fibonacci substitution map on words is defined by replacing each letter with a fixed block; additive decomposition of counts under that map needs exactly these cons identities.
Upstream edges into Nat addition associativity and commutativity (and parallel add lemmas in the foundation arithmetic layers) appear only as simp fuel for reordering the successor term after unfolding the count.
proof idea
One-line wrapper: simp with the recursive definition of the true-count together with Nat.add_comm, Nat.add_left_comm, and Nat.add_assoc. Unfolding the true-head clause produces a successor of the recursive count; the Nat lemmas put that successor into the form count + 1.
why it matters
Feeds the parent lemma on additive count decomposition under Fibonacci substitution: counts on a substituted word split as true-count equals the old false-count and false-count equals the sum of both old counts. That decomposition is the bridge from the two-letter substitution rules to Fibonacci recurrences on letter tallies, which is the verification content of this necessity module.
In the broader Recognition stack this is scaffolding arithmetic for discrete combinatorial checks, not a forcing-chain landmark (T5–T8). It closes a tiny but necessary simp API so induction on substituted words does not stall on successor arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.