sumFirst
plain-language theorem explainer
sumFirst counts the number of true bits in the initial segment of length m of a boolean stream. Lemmas on cylinder agreement and non-negativity in the Streams module cite it when equating finite sums to Z_of_window. The definition is a direct Finset summation over Fin m using an indicator function.
Claim. Let $s : ℕ → Bool$ be a stream. Define $sumFirst(m, s) := ∑_{i=0}^{m-1} [s(i)]$, where $[true] = 1$ and $[false] = 0$.
background
The Streams module treats periodic extensions and finite sums over boolean sequences. Stream is the type Nat → Bool. sumFirst extracts the integer count of true entries in the prefix of length m. Upstream structures such as PhiForcingDerived.of supply the J-cost context in which these counts later appear as defect measures.
proof idea
Definition, not theorem. The body is the one-line Finset sum ∑ i : Fin m, (if s i.val then 1 else 0).
why it matters
Feeds lemmas sumFirst_eq_Z_on_cylinder, sumFirst_nonneg, sumFirst8_extendPeriodic_eq_Z and the Measurement abbrev. Supports the eight-tick octave (T7) by enabling exact prefix counts on periodic 8-bit windows and cylinder sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.