subBlockSum8
plain-language theorem explainer
subBlockSum8 computes the integer sum of bits in one 8-tick window of a boolean Stream, offset by j full blocks. Measurement-layer proofs that equate aligned sums to the window integer Z on cylinders or periodic extensions cite this definition. It is a direct one-line alias to the underlying MeasurementLayer implementation.
Claim. Let $s$ be a Stream and $j$ a natural number. Then subBlockSum8$(s,j)$ equals the sum of the indicator function over the eight consecutive positions starting at index $8j$, that is, $subBlockSum8(s,j) = sum_{i=0}^7 1_{s(8j+i)}$.
background
The Measurement module re-exports eight-tick stream invariants together with a lightweight continuous-time measurement scaffold. Stream is the alias for PatternLayer.Stream, the boolean streams on which window sums are evaluated. Upstream, tick denotes the fundamental RS time quantum with the explicit remark that one octave equals eight ticks, the fundamental evolution period. Related upstream structures include LedgerFactorization for J-cost calibration and SpectralEmergence for the emergence of gauge content and fermion counts from the same discrete framework.
proof idea
one-line wrapper that applies MeasurementLayer.subBlockSum8
why it matters
This definition supplies the basic aligned 8-tick sum that downstream lemmas firstBlockSum_eq_Z_on_cylinder and subBlockSum8_periodic_eq_Z rely on to prove equality with Z_of_window. Those lemmas in turn feed blockSumAligned8 and blockSumAligned8_periodic in Streams.Blocks. The construction directly instantiates the eight-tick octave (T7) of the forcing chain, enabling the measurement of discrete Z values on cylinder sets and periodic extensions that appear throughout the Recognition Science measurement layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.