firstBlockSum_eq_Z_on_cylinder
plain-language theorem explainer
The lemma states that any stream inside the cylinder of an 8-bit window has its initial 8-tick block sum equal to the window's one-count Z. Researchers formalizing eight-tick measurement invariants cite this when connecting pattern windows to block sums. The proof is a one-line wrapper that reduces via simplification to the corresponding statement in MeasurementLayer.
Claim. Let $w$ be a pattern of length 8 and let $s$ be a stream in the cylinder set of $w$. Then the sum of the first sub-block of length 8 in $s$ equals the integer $Z(w)$ that counts the ones in $w$.
background
The module re-exports eight-tick stream invariants for the measurement layer. Pattern n denotes a finite window of length n. Stream denotes a boolean sequence. Cylinder w is the set of streams matching the bits of w on the initial segment. Z_of_window w is the integer that counts the number of ones inside the window w.
proof idea
The proof is a one-line wrapper. It applies simpa to unfold the definitions of subBlockSum8, Cylinder and Z_of_window, then directly invokes the matching lemma firstBlockSum_eq_Z_on_cylinder from MeasurementLayer.
why it matters
This supplies the base equality for aligned block sums that downstream lemmas in Streams.Blocks (blockSum_equals_Z_on_cylinder_first and the re-exported firstBlockSum_eq_Z_on_cylinder) rely on. It anchors the eight-tick periodicity (T7) inside the measurement scaffold and links pattern windows to observable sums used in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.