sumFirst
plain-language theorem explainer
sumFirst counts the number of true bits among the first m positions of a Boolean stream. Measurement proofs on eight-tick windows cite it to obtain non-negativity and cylinder equalities. The declaration is realized as a direct one-line re-export of the PatternLayer implementation.
Claim. For a Boolean stream $s$ and natural number $m$, define the sum as the cardinality of positions $i$ with $0 ≤ i < m$ where $s(i)$ holds, equivalently $∑_{i=0}^{m-1} [s(i)]$ with Iverson bracket.
background
The Measurement module re-exports eight-tick stream invariants together with a lightweight continuous-time scaffold. Streams are Boolean sequences that record discrete excitations; the upstream tick definition sets the fundamental time quantum $τ_0 = 1$ and identifies one octave with eight ticks. This supplies the periodic window structure used by downstream cylinder and periodicity lemmas.
proof idea
One-line wrapper that delegates directly to PatternLayer.sumFirst.
why it matters
The definition supplies the basic counting operation for finite windows and feeds the parent results sumFirst_eq_Z_on_cylinder, sumFirst_nonneg and sumFirst8_extendPeriodic_eq_Z in the Streams module. It anchors the measurement layer to the eight-tick octave (T7) of the forcing chain and supports the discrete excitation counting required for the Recognition Science mass and spectral formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.