countFalse
plain-language theorem explainer
Counts how many false symbols appear in a finite boolean word. Anyone tracking symbol statistics under the two-letter Fibonacci substitution cites this counter. It is a plain structural recursion on lists: empty word gives zero, and each false head contributes one.
Claim. For a word $w$ over $\{\mathsf{false},\mathsf{true}\}$, write $\#_{\mathsf{false}}(w)$ for the number of occurrences of $\mathsf{false}$ in $w$. On the empty word this is $0$; on a nonempty word it adds $1$ exactly when the head is $\mathsf{false}$ and continues on the tail.
background
The module develops a two-letter substitution system whose symbol counts obey Fibonacci recurrences. Locally a word is just a finite list of booleans. The companion Fibonacci sequence is the standard one with $F(0)=0$, $F(1)=1$, and $F(n+2)=F(n+1)+F(n)$.
This definition supplies the basic false-count observable on which the substitution acts. A parallel true-count is defined beside it. Upstream, the same name Word appears in the Loom core as lists of signed cotree generators; here the abbreviation is independent and strictly boolean.
proof idea
Definition by structural recursion on the list, not a proved theorem. The empty clause returns $0$. The cons clause evaluates a boolean test on the head (one if false, zero if true) and adds the recursive call on the tail. No lemmas are invoked at the definition site; later simp lemmas unfold this recursion.
why it matters
The counter is the workhorse for the whole FibSubst development. Downstream simp facts (nil, cons-false, cons-true, append) and the iteration lemmas that relate successive substitution powers to Fibonacci numbers all mention it by name. Those facts feed the FibSubstCert structure, whose verification predicate states that Fibonacci counts emerge from substitution iteration. In the broader Recognition framework this sits in the verification/necessity layer that underwrites self-similar counting (phi-ladder and Fibonacci structure) rather than in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.