sumFirst_zero
plain-language theorem explainer
sumFirst_zero establishes that the partial sum over an empty prefix of a boolean stream is identically zero. Workers on inductive arguments over stream lengths in the measurement layer cite this as the zero case. The proof is a direct simplification from the summation definition.
Claim. For every boolean stream $s : Nat → Bool$, the sum of the first zero bits equals zero: $∑_{i ∈ Fin 0} (if s(i.val) then 1 else 0) = 0$.
background
The Streams module treats periodic extension and finite sums over boolean sequences. A Stream is the type Nat → Bool. sumFirst m s is defined as the summation ∑_{i : Fin m} (if s i.val then 1 else 0). This supplies the base case for induction on m. The definition is imported from the Measurement layer as an abbreviation over the PatternLayer sum.
proof idea
One-line wrapper that applies simp to the definition of sumFirst, which evaluates the empty sum directly to zero.
why it matters
This base case anchors inductive arguments on finite bit sums inside the Streams module. It supports later constructions such as Z_of_window and extendPeriodic8 that rely on prefix sums. The result sits at the arithmetic foundation for the eight-tick octave structure without invoking any anchor or mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.