sumFirst_eq_zero_of_all_false
A lemma establishing that the partial sum over the first m positions of a Boolean stream vanishes whenever every entry in that window is false. Researchers analyzing finite windows in periodic streams would cite it to reduce all-false cases during pattern counting. The proof unfolds the sum definition, applies functional extensionality to replace the indicator with the zero function via the hypothesis, and simplifies.
claimLet $s : ℕ → Bool$ be a stream and $m ∈ ℕ$. If $s(i) = false$ for all $i < m$, then $∑_{i=0}^{m-1} [s(i)] = 0$, where $[true] = 1$ and $[false] = 0$.
background
The Streams module develops tools for periodic extensions and finite sums over Boolean streams. A stream is an infinite display given by the definition Stream := Nat → Bool. The operation sumFirst computes the count of true entries in the initial segment of length m via the explicit sum ∑_{i : Fin m} (if s i.val then 1 else 0).
proof idea
The proof unfolds sumFirst to expose the sum of indicators. It then proves by funext and simp that the indicator function equals the constant zero function, using the hypothesis that every entry is false. A final simp reduces the sum of zeros to zero.
why it matters in Recognition Science
This lemma supplies the zero case for finite sums over streams, supporting reductions inside periodic-extension constructions such as extendPeriodic8. It fits the eight-tick octave framework by enabling clean handling of zero-defect windows. No direct parent theorems are listed among the used-by edges.
scope and limits
- Does not apply when any entry in the window is true.
- Does not address infinite sums or periodic extensions.
- Does not interact with J-cost, phi-ladder, or mass formulas.
- Does not supply bounds for nonzero windows.
formal statement (Lean)
115lemma sumFirst_eq_zero_of_all_false {m : Nat} {s : Stream}
116 (h : ∀ i : Fin m, s i.val = false) :
117 sumFirst m s = 0 := by
proof body
Tactic-mode proof.
118 unfold sumFirst
119 have : (fun i : Fin m => (if s i.val then 1 else 0)) = (fun _ => 0) := by
120 funext i; simp [h i]
121 simp [this]
122
123end Streams
124
125end IndisputableMonolith