blockSum_equals_Z_on_cylinder_first
plain-language theorem explainer
If a Boolean stream lies in the cylinder of an 8-bit window w, its first aligned 8-tick block sums exactly to the number of ones in w. Researchers reducing infinite streams to finite window functionals in the Recognition Science measurement layer cite this when handling periodic extensions. The proof is a one-line term that unfolds the aligned sum definition and invokes the first-block cylinder equality.
Claim. Let $w$ be a pattern of length 8 and let $s$ be a stream belonging to the cylinder set of $w$. Then the aligned sum over the first block of 8 ticks in $s$ equals $Z(w)$, where $Z$ counts the number of true entries in the window.
background
A Pattern n is a map from Fin n to Bool giving a finite window of length n. A Stream is a function Nat to Bool. The Cylinder of w collects all streams whose initial n bits match w exactly. Z_of_window w returns the integer sum of 1 for each true entry in the window. These sit inside the module that ports the Pattern and Measurement layers handling streams, windows, and aligned block sums.
proof idea
The proof is a term-mode one-liner. It applies classical, then simp on the definition of the aligned block sum together with the already-established first-block equality on the given cylinder membership.
why it matters
The lemma supplies the first-block case for sums on periodic 8-tick extensions, realizing the eight-tick octave (T7) inside the streams layer. It supports reduction of infinite streams to the finite Z functional used in anchor relations and complexity structure. No direct downstream theorems are recorded, yet it closes a measurement step required for the discrete tiering and J-cost minimization developed in upstream structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.