blockSumAligned8
plain-language theorem explainer
The definition computes the total number of true bits across the first 8k positions of a Boolean stream by summing the counts from each of k consecutive 8-tick blocks. Measurement-layer work in Recognition Science cites it when constructing finite-instrument observations at lengths that are multiples of the eight-tick octave. The definition is realized directly as a summation of the per-block count function over the initial k indices.
Claim. For a Boolean stream $s : ℕ → {0,1}$ and natural number $k$, the aligned block sum over $k$ consecutive 8-tick windows is $∑_{j=0}^{k-1}$ (count of true entries in the block of $s$ starting at position $8j$).
background
Streams.Blocks supplies the pattern and measurement layer for Boolean streams (infinite sequences $ℕ → Bool$) and finite 8-tick windows. The eight-tick window length originates in the T7 step of the unified forcing chain, where the fundamental period is fixed at $2^3$. Sub-block summation aggregates these windows to produce totals at instrument lengths $T = 8k$, exactly the setting required for averaged observations on periodic extensions.
proof idea
The definition is a direct one-line summation that applies the per-block count function to each index $j : Fin k$ and adds the results.
why it matters
The definition is invoked by the periodic lemma that recovers $k · Z(w)$ for any periodic extension of an 8-bit window and by the averaged-observation constructor observeAvg8. It therefore supplies the concrete measurement operation that realizes the DNARP equation at finite multiples of the eight-tick octave, closing the link from the T7 forcing step to observable block sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.