countTrue_append
plain-language theorem explainer
Counting true bits is additive under concatenation of boolean words. Anyone deriving Fibonacci count recurrences from a two-letter substitution cites this as the left-factor step. The proof is induction on the left word, with a boolean case split on the head and Nat addition commutativity/associativity rewrites.
Claim. Let $w_1,w_2$ be finite words over $\{\mathsf{false},\mathsf{true}\}$. Then the number of $\mathsf{true}$ letters in the concatenation $w_1{+\!+}w_2$ equals the sum of the numbers of $\mathsf{true}$ letters in $w_1$ and in $w_2$.
background
The module develops a two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is a finite list of booleans; countTrue is the number of true entries in that list (with the usual nil and cons recurrences as sibling lemmas).
Concatenation is ordinary list append. The lemma is the standard homomorphism property of a counting functional under append: totals on a join equal the sum of totals on the factors.
Upstream Nat addition facts (associativity, commutativity, left-commutativity) appear only to rearrange the successor arithmetic that arises when the head bit is true.
proof idea
Induct on the left word. The empty case is immediate by simplification of countTrue on nil and append. For a cons cell, case-split on the head boolean: if false, the count ignores the head and the inductive hypothesis applies directly; if true, the count contributes one plus the inductive hypothesis, and Nat.add_comm, Nat.add_left_comm, and Nat.add_assoc realign the summands so both sides match.
why it matters
This is the append-homomorphism step used by counts_sub_word, which states that counts on a Fibonacci-substituted word decompose additively: false-count after substitution equals total length of the source word, and true-count after substitution equals the source false-count. That decomposition is the bridge from single-symbol substitution rules to the global Fibonacci recurrence on letter counts in the Verification.Necessity layer.
Within Recognition Science this sits in the verification stack that checks combinatorial necessities feeding the forcing chain (eight-tick structure, self-similar phi scaling), not in the analytic T5–T8 uniqueness arguments themselves. It closes a small but load-bearing counting identity so the substitution analysis can stay sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.