blockSumAligned8
plain-language theorem explainer
blockSumAligned8 defines the total count of true bits summed across k consecutive 8-tick blocks of a boolean stream. Measurement-layer authors cite it when instrument length equals 8k. The definition is the direct sum of subBlockSum8 over the k blocks indexed by Fin k.
Claim. For a stream $s : ℕ → Bool$ and $k ∈ ℕ$, the aligned block sum is $∑_{j=0}^{k-1} subBlockSum8(s, j)$.
background
A Stream is the infinite boolean sequence ℕ → Bool. Patterns are finite 8-bit windows. The module supplies the pattern and measurement layers for streams, windows, and aligned block sums, porting the PatternLayer/MeasurementLayer cluster. subBlockSum8 extracts the count inside each 8-tick window starting at offset 8j. Breath1024.T supplies the fundamental period as a natural number.
proof idea
One-line definition that sums subBlockSum8 over the first k blocks via the Fin k index set.
why it matters
This definition is invoked by blockSumAligned8_periodic and observeAvg8 to obtain k · Z(w) on periodic extensions and to define the per-window average. It implements the eight-tick octave (T7) inside the streams layer and supports the DNARP equation that equates averaged observations to the window integer Z.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.