observeAvg8_periodic_eq_Z
plain-language theorem explainer
The lemma shows that for any nonzero k and any 8-bit pattern w, the k-block averaged observation on the periodic extension of w equals Z(w), the integer count of ones inside w. Measurement theorists reducing periodic stream data to window statistics would cite this equality to collapse block sums directly to pattern counts. The proof unfolds the average, applies the aligned block-sum identity, cancels the factor k via the nonzero hypothesis, and finishes by simplification.
Claim. Let $w$ be any pattern of length 8 and let $k$ be a positive integer. Then the averaged observation over $k$ aligned blocks of the periodic extension of $w$ equals $Z(w)$, where $Z(w)$ is the number of ones in the window.
background
Pattern is the type of finite windows: a function from Fin n to Bool. Z_of_window sums the ones inside such a window, returning a natural number. extendPeriodic8 repeats the 8-bit window indefinitely to produce a stream. observeAvg8 computes the per-window average of the block sum over the first k aligned 8-blocks of a stream. The module supplies the Pattern and Measurement layers that formalize streams, windows, and aligned block sums. The key upstream fact is blockSumAligned8_periodic, which states that the sum of k aligned 8-blocks on the periodic extension equals k times Z_of_window(w).
proof idea
The tactic proof first invokes classical, unfolds observeAvg8, obtains the block-sum identity blockSumAligned8_periodic w k, proves the auxiliary equality (k * Z_of_window w) / k = Z_of_window w by Nat.mul_div_cancel_left using hk, and concludes with simpa using those two facts.
why it matters
This equality supplies the DNARP relation that equates averaged observations on periodic 8-bit streams to the window integer Z. It is invoked by the corresponding statement in the Measurement module, closing the reduction from block sums to pattern counts. The result sits inside the measurement scaffolding that links periodic extensions to the integer anchor Z used in mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.