sumFirst_eq_Z_on_cylinder
plain-language theorem explainer
Streams whose initial segment matches a finite pattern window have their prefix sum equal to the window's one-count Z. Measurement-layer proofs in the Recognition Science streams module cite this equality when aligning block sums to integer functionals. The tactic proof proceeds by classical unfolding of the definitions followed by a function extensionality step that equates the indicator functions pointwise.
Claim. If a stream $s$ lies in the cylinder set generated by a pattern $w$ of length $n$, then the sum of the first $n$ bits of $s$ equals the integer $Z$ counting the ones in $w$.
background
Pattern $n$ is the type Fin $n$ → Bool for finite bit windows. Stream is the type Nat → Bool for infinite sequences. Cylinder $w$ is the set of streams whose first $n$ positions match $w$ exactly. Z_of_window $w$ is the sum over Fin $n$ of the indicator (1 if true, 0 otherwise), while sumFirst $n$ $s$ computes the same sum on the stream prefix.
proof idea
The tactic proof opens with classical, unfolds sumFirst, Z_of_window, and Cylinder, then uses funext to equate the two indicator functions pointwise from the cylinder membership hypothesis, after which simpa closes the goal.
why it matters
This lemma is invoked by the re-exported sumFirst_eq_Z_on_cylinder in the parent Streams module and by firstBlockSum_eq_Z_on_cylinder for aligned 8-bit blocks. It supplies the direct reduction from stream prefixes to window integers, supporting measurement alignment with the eight-tick octave and phi-ladder mass formulas in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.