counts_sub_word
plain-language theorem explainer
After the two-letter Fibonacci substitution is applied letterwise to any Boolean word, the false-count of the image equals the total length of the original word, and the true-count equals the original false-count. Anyone tracking Fibonacci growth of letter counts under iteration cites this. The proof is structural induction on the word, using the two single-letter count lemmas and additivity of counts under concatenation.
Claim. For every finite Boolean word $w$, if $w'$ is the word obtained by applying the Fibonacci substitution letterwise to $w$, then $\#_0(w') = \#_0(w) + \#_1(w)$ and $\#_1(w') = \#_0(w)$.
background
The module studies a classical two-letter substitution system whose letter counts obey Fibonacci recurrences. A word is a finite list of Booleans. The substitution sends each letter to a short fixed block (fibSub), and fibSubWord is the concatenation of those blocks over the whole word (flatMap).
countFalse and countTrue are the ordinary letter counters. The single-letter base facts already fix the images: the false block contributes one false and one true, while the true block contributes one false and zero trues. The present lemma lifts those base counts to arbitrary words by additivity under concatenation.
The local setting is purely combinatorial: no Recognition-cost functional or continuum limit is invoked here. Natural-number addition is used only through its associative and commutative laws.
proof idea
Structural induction on the list w. The empty word is immediate by simplification of fibSubWord.
For a cons cell, case-split on the head bit. Unfold fibSubWord so the image is the single-letter block concatenated with the image of the tail. Invoke the corresponding single-letter count lemma (counts_sub_false or counts_sub_true), then rewrite with the append-count lemmas and the inductive hypothesis. A short burst of Nat.add_comm / add_left_comm / add_assoc rearranges the sums into the claimed form.
why it matters
This is the one-step bridge from letterwise substitution to the global Fibonacci recurrence on counts. The immediate consumer is counts_iter_succ, which states that one further iteration of the seed word updates the two counters exactly by the same additive rule; that lemma is a one-line unfold-and-rewrite once the present result is available.
In the Verification/Necessity layer the Fibonacci substitution supplies the discrete skeleton whose growth rates later match the golden-ratio fixed point forced at T6. Closing the count recurrence here is therefore a necessary combinatorial step before any claim that iterated recognition words produce $\varphi$-scaled populations. The lemma itself is fully proved (no sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.