subBlockSum8
plain-language theorem explainer
subBlockSum8 counts the number of true entries in the 8-tick window of a boolean stream that begins at index 8j. Pattern and measurement routines cite it when equating aligned block counts to the integer Z of a window. The definition is a direct finite sum that converts each Bool at the offset positions into 0 or 1.
Claim. Let $s : {0,1}^ℕ$ be a stream. For $j ∈ ℕ$, subBlockSum8$(s,j) = ∑_{i=0}^7 [s(8j + i)]$, where $[true] = 1$ and $[false] = 0$.
background
A Stream is the type ℕ → Bool, an infinite boolean sequence that models discrete time series in the pattern layer. The module implements aligned block sums over 8-tick windows; the constant tick supplies the fundamental time quantum τ₀ = 1, and one octave equals eight ticks. Upstream results include the structure of nuclear densities in phi-tiers and the ledger factorization that calibrates J-cost.
proof idea
one-line definition that applies summation over Fin 8, mapping each boolean value at offset j*8 + i.val to 1 or 0.
why it matters
This supplies the primitive counting operation used by blockSumAligned8 and firstBlockSum_eq_Z_on_cylinder to reduce aligned sums to Z_of_window. It realizes the eight-tick alignment required by the T7 octave of the unified forcing chain, allowing periodic stream measurements to collapse to window invariants in the measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.