sumFirst_zero
The lemma establishes that the sum of the first zero bits of any boolean stream equals zero. Researchers working on finite prefixes and inductive arguments in the Recognition Science measurement layer cite this as the base case for stream sums. The proof is a one-line simplification that unfolds the summation definition over the empty index set Fin 0.
claimFor any stream $s : ℕ → Bool$, the sum of its first zero bits is zero: $∑_{i : Fin 0} (if s(i.val) then 1 else 0) = 0$.
background
The Streams module develops periodic extensions and finite sums over boolean streams, where Stream is the type Nat → Bool. The function sumFirst m s is defined as the summation ∑_{i : Fin m} (if s i.val then 1 else 0), which counts the number of true bits in the initial segment of length m. This zero-length case supplies the empty-sum identity required for induction on window lengths.
proof idea
The proof is a one-line term-mode wrapper that applies the simp tactic to the sumFirst definition, reducing the empty sum over Fin 0 to the standard identity that summation over an empty finite set equals zero.
why it matters in Recognition Science
This base case anchors inductive arguments on finite windows inside the same module, such as the Z_of_window family that maps stream prefixes to integer anchors. It supports the measurement layer's handling of eight-tick periodic blocks without introducing extra hypotheses. No downstream uses are recorded yet, but the result closes the zero case for all subsequent sum identities.
scope and limits
- Does not compute or bound sums for any positive length m.
- Does not assume or enforce periodicity on the stream.
- Does not reference J-cost, phi-ladder, or anchor sectors.
- Does not extend to infinite sums or limits.
formal statement (Lean)
72@[simp] lemma sumFirst_zero (s : Stream) : sumFirst 0 s = 0 := by
proof body
Term-mode proof.
73 simp [sumFirst]
74
75/-- If a stream agrees with a window on its first `n` bits, then the first‑`n` sum equals `Z`. -/