Z_of_window
plain-language theorem explainer
Z_of_window supplies the integer count of true entries inside a finite boolean pattern of length n. Measurement and stream lemmas cite it when equating block sums on periodic extensions or cylinders to multiples of this count. The implementation is the direct summation of the indicator function over the finite index set.
Claim. Let $w :$ Fin $n$ $→$ Bool. Then $Z(w) :=$ ∑_{i : Fin n} (1 if $w(i)$ else 0).
background
The Streams.Blocks module defines patterns as maps from Fin n to Bool, representing finite windows on streams. It focuses on streams, windows, and aligned block sums, porting the PatternLayer and MeasurementLayer cluster. Z_of_window is the integer functional counting ones in such a window. The Measurement abbrev reexports the identical definition from PatternLayer. Upstream results include structures for J-cost minimization (convex minimum at x=1) and spectral emergence (SU(3)×SU(2)×U(1) content and 24 chiral flavors).
proof idea
This is a definition that directly implements the sum: for each i in Fin n add 1 if the pattern bit w i is true, otherwise 0. It is the primitive implementation of the window count with no lemmas applied.
why it matters
Z_of_window is the foundational counting map feeding lemmas such as blockSumAligned8_periodic, firstBlockSum_eq_Z_on_cylinder, and observeAvg8_periodic_eq_Z. These establish that observations on cylinders and periodic 8-extensions recover exactly Z(w). It anchors the measurement layer to the eight-tick octave (period 2^3) in the forcing chain, enabling DNARP equations for averaged observations on streams.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.