sumFirst_nonneg
plain-language theorem explainer
The lemma shows that the sum of the first m bits of any boolean stream is non-negative. Workers on finite-window measurements and periodic patterns in Recognition Science cite it as a basic positivity fact for stream sums. The proof is a one-line wrapper that unfolds sumFirst and invokes Finset.sum_nonneg with a case split on each indicator term.
Claim. For every natural number $m$ and every stream $s : ℕ → {true, false}$, $0 ≤ ∑_{i=0}^{m-1} b_i$ where $b_i = 1$ if $s(i)$ holds and $b_i = 0$ otherwise.
background
The Streams module treats streams as infinite boolean sequences for periodic extensions and finite sums. Stream is the type Nat → Bool. sumFirst(m, s) is defined as the Finset sum over i : Fin m of (1 if s i.val else 0). The module documentation frames this as the setting for periodic extension and finite sums over such streams. The lemma depends on the identical Stream and sumFirst definitions imported from Measurement and from the Blocks submodule.
proof idea
Unfold sumFirst to expose the Finset sum of indicators. Apply Finset.sum_nonneg. For each index i the split tactic branches on whether s i.val is true or false; both branches are discharged by norm_num, which confirms the indicator is 0 or 1.
why it matters
The result supplies the elementary non-negativity needed for all subsequent finite-sum arguments over streams. It supports the measurement layer that feeds the eight-tick octave and phi-ladder constructions in the Recognition framework. No downstream theorems are recorded in the current graph, indicating it functions as a foundational closure for positivity in the Streams module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.