countTrue_nil
plain-language theorem explainer
The empty Boolean word contributes zero true symbols under the standard count. Anyone proving Fibonacci recurrences for 2-letter substitutions cites this as the nil base case. The proof is pure definitional equality (rfl) from the recursive clause of the count.
Claim. If $w$ is the empty Boolean word, then the number of $\mathrm{true}$ symbols in $w$ equals $0$.
background
The module studies a two-letter substitution system whose symbol counts obey Fibonacci recurrences. Locally a word is just a finite list of Booleans (List Bool), not the Loom cotree word type.
countTrue is the obvious recursive tally: empty list maps to 0; on a cons cell it adds 1 precisely when the head is true, then recurses. The companion countFalse and the four cons lemmas sit beside this nil fact and together give a complete simp suite for the two counters.
Upstream, the definition of countTrue already hard-codes the empty case as 0, so the lemma merely externalizes that clause for rewriting.
proof idea
One-line definitional proof: rfl matches the first equation of countTrue, which is | [] => 0. No lemmas are applied; the @[simp] attribute simply exposes that equation to the simplifier.
why it matters
Inside Verification.Necessity.FibSubst this is the nil base for all later count identities that feed Fibonacci substitution arguments. Those arguments support necessity claims about discrete counting structure in the Recognition stack (period and ladder bookkeeping adjacent to the eight-tick octave and phi-ladder). No downstream theorem is wired yet in the graph, so the lemma is infrastructure rather than a cited bridge theorem. It closes no open scaffold; it only makes the empty-word case automatic under simp.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.