countFalse_cons_false
plain-language theorem explainer
Prepending a false bit to a boolean word raises the false-count by exactly one. Anyone tracking letter counts under the Fibonacci substitution uses this as a base case. The proof is a one-line simp expansion of the recursive count definition plus natural-number addition commutativity and associativity.
Claim. For every boolean word $w$, the number of $\mathrm{false}$ entries in $\mathrm{false}::w$ equals the number of $\mathrm{false}$ entries in $w$ plus one.
background
The module studies a two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is a finite list of booleans. The false-count of a word is the number of false entries, defined by recursion on the list: empty word contributes zero, and each head bit adds one or zero according to its value.
The same module defines the companion true-count and the Fibonacci substitution map on words. Those maps act letterwise, so inductive arguments on words need clean cons-rules for both counters. Upstream arithmetic lemmas supply the addition identities that simp rewrites against when the recursive clause is unfolded.
proof idea
One-line wrapper: simp unfolds the recursive definition of the false-count on a cons cell whose head is false, then normalizes the resulting natural-number sum with Nat.add_comm, Nat.add_left_comm, and Nat.add_assoc. No induction or case split is required.
why it matters
Feeds the inductive step of counts_sub_word, which states that false- and true-counts decompose additively under the Fibonacci substitution: the substituted false-count equals the sum of the original counts, and the substituted true-count equals the original false-count. That additive law is the bridge from the two-letter substitution system to Fibonacci recurrences on letter counts, the local necessity claim of the module. Within Recognition Science verification, such count identities support the discrete combinatorial side of the forcing chain rather than the continuous J-cost or phi-ladder layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.