counts_sub_true
plain-language theorem explainer
The Fibonacci substitution sends the symbol true to the singleton word [false], so that word has false-count 1 and true-count 0. Anyone proving additive count laws for the full substitution morphism cites this base case. The argument is a one-line simplification against the single-symbol substitution definition.
Claim. Let $\sigma$ be the Fibonacci substitution on Boolean symbols with $\sigma(\mathsf{true})=[\mathsf{false}]$. Then the number of $\mathsf{false}$ symbols in $\sigma(\mathsf{true})$ equals $1$ and the number of $\mathsf{true}$ symbols equals $0$.
background
The module develops a two-letter substitution system on Boolean words whose letter counts obey Fibonacci recurrences. A word is a list of Booleans. The single-symbol Fibonacci substitution is defined by $\sigma(\mathsf{false})=[\mathsf{false},\mathsf{true}]$ and $\sigma(\mathsf{true})=[\mathsf{false}]$; it extends to words by concatenation.
Two structural-recursive counters tally occurrences: the false-count adds one on each false head, and the true-count adds one on each true head. Both return zero on the empty word. This lemma records the counts on the image of the symbol true, the simpler of the two single-symbol base cases needed before lifting to arbitrary words.
proof idea
One-line term-mode proof: simp [fibSub] unfolds the substitution on true to the singleton [false]. The recursive clauses of the two counters then evaluate immediately, giving false-count 1 and true-count 0.
why it matters
Downstream, counts_sub_word uses this fact (together with the false-symbol twin) inside a list induction to prove that counts on substituted words decompose additively: the false-count of $\sigma(w)$ equals the length of $w$, and the true-count of $\sigma(w)$ equals the false-count of $w$. That additive law is the combinatorial engine of the Fibonacci recurrences on letter counts under iterated substitution.
In the Recognition Science verification stack, such discrete counting identities support necessity arguments that structures forced by the framework exhibit Fibonacci growth, consistent with the self-similar fixed point $\varphi$ from the forcing chain (T6) and the $\varphi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.