sumFirst_eq_Z_on_cylinder
plain-language theorem explainer
A stream agreeing with a finite pattern on its initial n bits has its partial sum equal to the window's one-count Z. Pattern-matching arguments in the measurement layer cite this to equate cylinder membership with integer functionals. The tactic proof unfolds the three definitions, applies functional extensionality to the indicator functions, and simplifies using the cylinder hypothesis.
Claim. Let $w$ be a pattern of length $n$ and let $s$ be a stream lying in the cylinder set of $w$. Then the sum of the first $n$ bits of $s$ equals the integer $Z$ of the window $w$.
background
Pattern is the type of finite Boolean sequences of length $n$. Stream is the type of infinite Boolean sequences. Cylinder w is the set of all streams that match w exactly on the first $n$ positions. Z_of_window w is the sum over i in Fin n of the indicator (1 if w i is true). sumFirst n s is the analogous sum of the first n bits of s.
proof idea
The proof unfolds sumFirst, Z_of_window and Cylinder. It then proves the two indicator functions on Fin n are identical by funext and simp using the membership hypothesis hs at each i. A final simp closes the equality of the two Nat sums.
why it matters
The lemma is invoked directly by firstBlockSum_eq_Z_on_cylinder in Streams.Blocks, which specializes the result to 8-bit windows under periodic extension. It supplies the basic interface between cylinder membership and the integer Z used in anchor and mass calculations, supporting the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.