blockSumAligned8_periodic
The lemma states that for any 8-bit pattern w and natural k, the sum of k aligned 8-blocks on the periodic extension of w equals k times Z(w), the integer count of ones in w. Researchers deriving averaged observations from periodic streams in the Recognition Science measurement layer cite it to obtain integer results from 8-tick signals. The proof is a one-line simpa that unfolds the definitions and delegates to the MeasurementLayer version.
claimFor any pattern $w$ of length 8 and natural number $k$, the sum of $k$ aligned 8-blocks in the periodic extension of $w$ equals $k$ times $Z(w)$, where $Z(w)$ is the integer counting the number of ones in $w$.
background
Pattern 8 is the type of finite binary windows of length 8. Z_of_window is the integer functional that counts the ones inside such a window. extendPeriodic8 builds the infinite stream that repeats the window indefinitely. blockSumAligned8 sums the values of k consecutive aligned 8-blocks inside a stream. The module re-exports eight-tick stream invariants together with a lightweight continuous-time measurement scaffold. This lemma sits inside the local setting of periodic 8-tick signals whose sums are forced to be integer multiples of the window count.
proof idea
One-line wrapper that applies simpa to the definitions of blockSumAligned8, extendPeriodic8 and Z_of_window, then hands the goal to the corresponding lemma in MeasurementLayer.
why it matters in Recognition Science
The result is used directly by blockSumAligned8_periodic and observeAvg8_periodic_eq_Z in Streams.Blocks to obtain the DNARP equation (averaged observation equals Z on periodic extensions). It supplies the integer observation step required by the eight-tick octave (T7) and the mass-ladder formulas that place Z on the phi-ladder. The lemma therefore closes one link between the periodic stream invariants and the downstream claim that 8-tick periodic signals yield exact integer counts.
scope and limits
- Does not apply to non-periodic streams.
- Does not compute Z for windows of length other than 8.
- Does not address the continuous-time CQ score.
- Does not derive the value of Z from first principles.
Lean usage
have hsum := blockSumAligned8_periodic w kformal statement (Lean)
57lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
58 blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
proof body
Term-mode proof.
59 simpa [blockSumAligned8, extendPeriodic8, Z_of_window]
60 using MeasurementLayer.blockSumAligned8_periodic (w:=w) k
61
62/-- DNARP Eq.: on periodic extensions of an 8-bit window, the averaged observation equals `Z`. -/