blockSumAligned8_periodic
plain-language theorem explainer
The lemma shows that for any length-8 window w and natural k, the sum of k aligned 8-blocks on the periodic extension of w equals k times Z(w), the integer counting ones in w. Stream analysts deriving averaged observations in Recognition Science cite it to connect block sums to window invariants. The proof is a one-line simplification that delegates to the MeasurementLayer counterpart after unfolding the relevant definitions.
Claim. Let $w$ be a finite binary window of length 8 and let $k$ be a natural number. Then the sum of $k$ aligned blocks of length 8 taken from the periodic extension of $w$ equals $k$ times $Z(w)$, where $Z(w)$ counts the number of ones inside $w$.
background
Pattern n is the type of finite binary windows of length n. Z_of_window is the integer functional that counts the ones inside such a window. The Measurement module re-exports eight-tick stream invariants together with a lightweight continuous-time measurement scaffold based on CQ scores.
proof idea
The proof is a one-line wrapper. It applies simpa to unfold blockSumAligned8, extendPeriodic8 and Z_of_window, then invokes the corresponding lemma blockSumAligned8_periodic from MeasurementLayer.
why it matters
This lemma supplies the block-sum identity used by observeAvg8_periodic_eq_Z to obtain the DNARP equation (averaged observation equals Z on periodic 8-tick extensions). It therefore closes an invariant required by the eight-tick octave (T7) inside the forcing chain. The downstream copy in Streams.Blocks re-exports the same identity for block-processing pipelines.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.