countTrue
plain-language theorem explainer
Counts how many true bits appear in a finite Boolean word. Used throughout the Fibonacci substitution verification stack to track the true-count half of the (false,true) pair that obeys the Fibonacci recurrence. Defined by structural recursion on the list: empty word contributes 0; a head bit contributes 1 iff it is true, then recurse on the tail.
Claim. For a finite word $w$ over $\{\mathrm{false},\mathrm{true}\}$, $\mathrm{countTrue}(w)$ is the number of positions equal to $\mathrm{true}$. Explicitly: $\mathrm{countTrue}([])=0$ and $\mathrm{countTrue}(b::bs)=\mathbf{1}_{b=\mathrm{true}}+\mathrm{countTrue}(bs)$.
background
The module studies a two-letter substitution system on Boolean words whose symbol counts obey Fibonacci recurrences. A word is simply a finite list of Booleans. The companion counter countFalse tallies false symbols; together the pair (countFalse, countTrue) is the observable that the substitution dynamics act on.
The Fibonacci substitution replaces false by the block [false, true] and true by [false]. Iterating from a seed word and reading off the two counts produces the classical Fibonacci sequence. The present definition is the true-half of that counting map; every later lemma about iteration or substitution additivity is stated in terms of it.
Upstream, the local Word abbreviation is List Bool (distinct from the Loom.Core Word of signed cotree generators). No external arithmetic is required beyond Nat addition and a Boolean equality test.
proof idea
Pure structural definition, not a proved theorem. Pattern-match on the list: the empty word maps to 0; a cons cell adds 1 when the head equals true and 0 otherwise, then adds the recursive call on the tail. No lemmas are invoked; the body is the recursive equation itself.
why it matters
This counter is the primitive used by every Fibonacci-count lemma in the module. Downstream, counts_sub_false and counts_sub_true evaluate it on single-symbol substitutions; counts_sub_word and countTrue_append give additivity; counts_iter_succ and counts_iter_fib lift those facts to the full iteration, proving that after n steps from [false] one obtains (F_{n+1}, F_n). The certificate structure FibSubstCert packages exactly that emergence of Fibonacci counts from substitution iteration. In the broader Recognition verification layer it supplies a machine-checked witness that a concrete combinatorial dynamics realises the Fibonacci ladder used elsewhere in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.