blockSumAligned8_periodic
plain-language theorem explainer
The lemma states that summing k aligned 8-blocks on the periodic extension of any 8-bit pattern w equals k times the number of ones in w. Researchers modeling periodic stream observations or deriving averaged measurements in Recognition Science cite this for the DNARP relation. The proof works by showing each sub-block sum is constantly Z(w) via the periodic sub-block lemma, then applying Finset cardinality and constant-sum rules to scale by k.
Claim. Let $w$ be a finite pattern of length 8 and let $k$ be a natural number. For the infinite stream obtained by repeating $w$ periodically, the sum of the first $k$ aligned 8-blocks equals $k$ times the integer count of ones in $w$.
background
In the Streams.Blocks module, a Pattern of length n is a finite window given by a function from Fin n to Bool. Z_of_window counts the number of true entries in such a window, yielding an integer that later anchors mass formulas. extendPeriodic8 repeats the 8-bit window indefinitely to produce a bi-infinite stream, while blockSumAligned8 totals the ones across k consecutive aligned 8-blocks starting at multiples of 8.
proof idea
The tactic proof first unfolds blockSumAligned8, then uses subBlockSum8_periodic_eq_Z to prove every sub-block sum equals the constant Z_of_window w. It next invokes the cardinality of Fin k together with the Finset sum-of-constants identity to obtain the factor k, and finally composes the two equalities via congrArg and transitivity.
why it matters
This lemma supplies the key step for observeAvg8_periodic_eq_Z, which states that the per-window averaged observation on a periodic 8-stream equals Z(w). It thereby realizes the DNARP equation at the eight-tick scale and connects directly to the T7 octave in the forcing chain, where periodic repetition of length 2^3 appears in measurement averaging. The result closes one link between stream observations and the integer Z functional used in anchor relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.