blockSumAligned8
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply to windows whose length is not a multiple of 8.
- Does not incorporate J-cost, phi-ladder scaling, or continuous limits.
- Does not handle non-Boolean or non-periodic streams beyond the cylinder condition.
- Does not compute infinite sums or asymptotic densities.
formal statement (Lean)
75def blockSumAligned8 (k : Nat) (s : Stream) : Nat :=
proof body
Definition body.
76 ∑ j : Fin k, subBlockSum8 s j.val
77
78/-- On any stream lying in the cylinder of an 8‑bit window, the aligned
79 first block sum (j=0; T=8k alignment) equals the window integer `Z`. -/