Z_of_window
plain-language theorem explainer
The window count function tallies the number of 1-bits inside an n-length pattern. Measurement lemmas on periodic extensions and cylinders cite this count to equate block sums and averaged observations to the pattern content. The declaration is a one-line alias to the underlying layer implementation.
Claim. For a finite pattern $w$ of length $n$, let $Z(w)$ denote the integer equal to the number of indices where the pattern entry equals 1.
background
The module re-exports eight-tick stream invariants for measurement, together with a lightweight continuous-time scaffold. Pattern denotes the type of finite windows of length $n$. The window count function extracts the integer tally of 1-bits from any such window, matching the supplied doc-comment on the integer functional.
proof idea
One-line wrapper that applies the PatternLayer implementation of the window count.
why it matters
The definition supplies the count referenced by downstream lemmas including blockSumAligned8_periodic, firstBlockSum_eq_Z_on_cylinder, observeAvg8_periodic_eq_Z, and sumFirst_eq_Z_on_cylinder. These establish equality of block sums to the window count on periodic extensions and cylinders, supporting the eight-tick octave invariants (T7) inside the measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.