sumFirst
plain-language theorem explainer
The definition counts the number of true entries among the first m positions of a boolean stream s. Workers on periodic pattern sums and cylinder reductions cite it when equating finite bit counts to Z_of_window values. The body is a direct Finset summation that maps true to 1 and false to 0.
Claim. For a stream $s : ℕ → Bool$, define the partial sum $∑_{i=0}^{m-1} s(i)$ where each true value contributes 1 and each false value contributes 0.
background
The Streams module develops tools for periodic extension and finite sums over boolean streams. Stream is the type Nat → Bool, an infinite display of boolean values. The definition supplies the basic counting operation that later lemmas apply to windows and cylinders.
proof idea
One-line definition that expands directly to the Finset sum over Fin m, with the indicator (if s i.val then 1 else 0).
why it matters
This definition is the common base for downstream results including sumFirst_eq_Z_on_cylinder, sumFirst8_extendPeriodic_eq_Z, sumFirst_nonneg and sumFirst_zero. It supports the module's treatment of eight-tick periodic structures and finite sums that appear in pattern-to-Z reductions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.