observeAvg8_periodic_eq_Z
plain-language theorem explainer
The lemma equates averaged observations on periodic extensions of 8-bit windows to the integer one-count Z of the window. Measurement theorists working with eight-tick stream invariants cite it when connecting block averages to pattern functionals. The proof is a one-line simplification that delegates to the core layer theorem after unfolding the re-exports.
Claim. For nonzero natural number $k$ and 8-bit pattern $w$, the averaged observation observeAvg8 applied to $k$ and the periodic extension of $w$ equals $Z(w)$, where $Z$ counts the ones in the window.
background
Pattern n is the type of finite windows of length n, realized as functions Fin n to Bool. Z_of_window is the integer functional that counts the true entries in such a window. extendPeriodic8 produces the infinite stream obtained by repeating the given 8-bit window. observeAvg8 returns the averaged per-window observation count over k aligned blocks of a stream. The module re-exports eight-tick stream invariants from the measurement layer together with a lightweight continuous-time measurement scaffold (CQ score).
proof idea
One-line wrapper that applies MeasurementLayer.observeAvg8_periodic_eq_Z after unfolding the re-exported definitions observeAvg8, extendPeriodic8 and Z_of_window via simpa.
why it matters
This lemma supplies the DNARP equation on periodic extensions of 8-bit windows inside the measurement layer. It is used by the corresponding statement in Streams.Blocks, which expands the equality to block sums. The result supports the eight-tick octave invariants by equating averaged observations to the window integer Z on periodic streams.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.