subBlockSum8
plain-language theorem explainer
subBlockSum8 counts the number of true entries in an 8-position window of a boolean stream s beginning at index 8j. Measurement and pattern-layer work cites it when reducing aligned block sums to the integer Z of a window. The definition is a direct finite sum that applies the indicator function over Fin 8 offsets.
Claim. For a stream $s : ℕ → Bool$ and $j ∈ ℕ$, subBlockSum8$(s,j) := ∑_{i=0}^7 1_{s(8j+i)}$, where the indicator $1$ returns 1 on true and 0 on false.
background
A Stream is the type Nat → Bool, an infinite boolean display used for patterns and measurements. The module sets up pattern and measurement layers that operate on streams, windows, and aligned block sums, porting earlier PatternLayer and MeasurementLayer material. Upstream results supply the tick constant (fundamental time quantum) and the convention that one octave equals 8 ticks, fixing the window length here.
proof idea
The declaration is a direct definition that unfolds as summation over the Fin 8 range, adding 1 precisely when the stream value at offset j*8 + i is true.
why it matters
This definition is the basic counting primitive that feeds the lemmas firstBlockSum_eq_Z_on_cylinder and blockSumAligned8_periodic, which equate sub-block sums to the window integer Z. It implements the 8-tick octave structure required by the forcing chain (T7) and supports reduction of periodic extensions to integer multiples of Z. No open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.