Z_of_window
plain-language theorem explainer
Z_of_window defines the integer count of true entries in a finite Boolean pattern of length n. Measurement and stream researchers cite it when equating block sums or periodic observations to the underlying window bit count. The definition is a direct summation that converts each Boolean to 1 or 0 and adds them over Fin n.
Claim. For a pattern $w : (Fin n) → Bool$, define $Z(w) := ∑_{i ∈ Fin n} [w(i)]$, where $[true] = 1$ and $[false] = 0$.
background
The Streams module treats periodic extensions of finite windows and the associated finite sums. Pattern is the type Fin n → Bool, a finite window of length n whose entries are Booleans. Z_of_window is the integer functional that counts the number of true entries in such a window.
proof idea
Direct definition: the body is the summation over i : Fin n of the Iverson bracket that returns 1 precisely when w i is true.
why it matters
This supplies the basic Z count used by downstream lemmas such as blockSumAligned8_periodic (block sums equal k · Z(w) on periodic extensions) and firstBlockSum_eq_Z_on_cylinder (first block sum equals Z on the cylinder of w). It anchors the DNARP equations and periodic observation equalities that appear throughout the Measurement layer. The definition therefore closes the interface between raw stream data and the integer functionals required for later mass and observation formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.