subBlockSum8_periodic_eq_Z
plain-language theorem explainer
For any 8-bit window w, the sum of bits in any aligned 8-block of its periodic extension equals the Hamming weight Z(w) of that window. Measurement proofs working with periodic eight-tick streams cite this to reduce every sub-block sum to a constant independent of starting index. The argument is a one-line simpa that unfolds the periodic extension and sub-block definitions then delegates to the core MeasurementLayer lemma.
Claim. Let $w$ be a finite pattern of length 8. Let $s$ be the infinite stream obtained by repeating $w$ periodically. For every natural number $j$, the sum of the eight consecutive bits of $s$ beginning at position $8j$ equals $Z(w)$, where $Z(w)$ is the number of 1-bits in $w$.
background
In the Measurement module, Pattern n is the type of finite windows of length n, i.e., maps from Fin n to Bool. Z_of_window w returns the integer count of true entries in such a window. extendPeriodic8 w builds the bi-infinite periodic stream that repeats the window indefinitely. subBlockSum8 s j returns the sum of the eight bits of s whose indices run from 8j to 8j+7.
proof idea
The proof is a one-line wrapper that applies simpa with the three definitions subBlockSum8, extendPeriodic8 and Z_of_window, then invokes the corresponding lemma already proved in MeasurementLayer. No case splits or additional hypotheses are introduced.
why it matters
The lemma is the direct reduction step used by blockSumAligned8_periodic in Streams.Blocks, which states that the sum of k aligned 8-blocks on the periodic extension equals k·Z(w). It supplies the local eight-tick periodicity invariant required by the measurement layer and thereby supports the T7 eight-tick octave in the forcing chain. No open scaffolding remains in the supplied dependencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.