sumFirst
plain-language theorem explainer
sumFirst counts the number of true bits in the initial segment of length m from a boolean stream s. Measurement proofs for cylinder agreement and periodic 8-bit extensions cite this when equating prefix counts to window values. It is realized directly as a finite sum over Fin m using the boolean indicator.
Claim. For a stream $s : {N} {to} {Bool}$ and $m {in} {N}$, the first-$m$ sum is $sum_{i=0}^{m-1} 1_{s(i)}$ where $1_{true}=1$ and $1_{false}=0$.
background
The Streams.Blocks module treats pattern and measurement layers for streams, windows, and aligned block sums, porting the PatternLayer/MeasurementLayer cluster. A Stream is defined as the infinite boolean display Nat to Bool. Upstream, the Z map from Masses.Anchor converts rational charges to integers via sector polynomials (Q6 squared plus Q6 to the fourth for leptons, plus constants for quarks), while earlier sumFirst versions in Streams supply the summation primitive for zero and nonnegativity lemmas.
proof idea
The definition is given directly by the summation over i : Fin m of (if s i.val then 1 else 0). No auxiliary lemmas are invoked; it is the primitive that downstream results unfold to apply Finset.sum_nonneg or funext for indicator rewriting.
why it matters
This definition is called by ten downstream results, among them sumFirst_eq_Z_on_cylinder (equating the prefix sum to Z_of_window under cylinder membership) and sumFirst8_extendPeriodic_eq_Z (for periodic 8-bit windows). It supplies the basic counting tool in the streams layer, supporting the eight-tick octave and anchor Z relations from the T0-T8 forcing chain while enabling mass-ladder comparisons via phi exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.