countFalse_append
plain-language theorem explainer
Concatenation of boolean words is additive for the false-count: the number of false bits in w₁ ++ w₂ equals the sum of the two separate counts. Anyone proving Fibonacci-type recurrences for 2-letter substitution systems cites this as the basic homomorphism property of the counter. The proof is a short induction on the first word with a case split on the head bit.
Claim. Let $w_1,w_2$ be finite words over $\{\mathsf{true},\mathsf{false}\}$. Then the number of $\mathsf{false}$ letters in the concatenation satisfies $\#_{\mathsf{F}}(w_1{+}{+}w_2)=\#_{\mathsf{F}}(w_1)+\#_{\mathsf{F}}(w_2)$.
background
The module studies a two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is simply a finite list of booleans. The false-count is the number of false entries in that list (with the obvious recursive clauses on nil and cons).
Additivity under concatenation is the elementary homomorphism property any such counter must satisfy before one can push counts through a substitution rule. The same module defines the companion true-count and the Fibonacci substitution map on words; those objects are not needed for the statement itself, only for the surrounding development.
Upstream arithmetic facts used in the proof are ordinary natural-number associativity and commutativity of addition (appearing via simp under several foundation aliases).
proof idea
Induct on the first word. The empty-list base case is immediate by simplification of the recursive definition of the false-count. In the cons step, case-split on the head boolean: if it is false, the count increments by one on both sides and the inductive hypothesis plus Nat.add_comm / Nat.add_left_comm / Nat.add_assoc rearrange the sum; if it is true, the count is unchanged and the inductive hypothesis alone finishes after simp.
why it matters
This lemma is the additive engine for counts_sub_word, which states that false- and true-counts of a Fibonacci-substituted word decompose as $#{\mathsf{F}}(\mathrm{fibSubWord},w)=#{\mathsf{F}}(w)+#{\mathsf{T}}(w)$ and $#{\mathsf{T}}(\mathrm{fibSubWord},w)=#_{\mathsf{F}}(w)$. That decomposition is the bridge from the local substitution rule to the global Fibonacci recurrence on letter counts.
In the Recognition verification layer the Fibonacci substitution supplies the discrete combinatorial skeleton behind the eight-tick octave and the self-similar $\varphi$-ladder (forcing steps T6–T7). Establishing that counts are strictly additive under concatenation is a necessary bookkeeping step before those recurrences can be certified inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.