subBlockSum8
plain-language theorem explainer
Measurement protocols in Recognition Science rely on this definition to extract the bit-sum over aligned 8-tick windows of a boolean stream. It appears in lemmas that equate such sums to the integer value Z of a pattern window when the stream lies in the corresponding cylinder. The implementation delegates immediately to the core layer function without additional computation.
Claim. For a boolean stream $s$ and natural number $j$, define the sub-block sum as $subBlockSum8(s,j) := sum_{i=0}^7 [s(j*8 + i)]$, where $[true]=1$ and $[false]=0$.
background
The module re-exports eight-tick stream invariants used for measurement, with Stream as an alias for PatternLayer.Stream (boolean sequences). The 8-tick window matches the fundamental octave from Constants.tick, where one octave equals 8 ticks and tau_0 = 1. Upstream structures include NucleosynthesisTiers.of placing nuclear densities on phi-tiers, PhiForcingDerived.of for J-cost, and SpectralEmergence.of deriving SU(3)xSU(2)xU(1) gauge content plus 24 chiral fermions from Q3 face-pair counts.
proof idea
This is a one-line wrapper that applies MeasurementLayer.subBlockSum8.
why it matters
This definition supports lemmas firstBlockSum_eq_Z_on_cylinder and subBlockSum8_periodic_eq_Z, which feed blockSumAligned8 and blockSumAligned8_periodic in Streams.Blocks. It realizes the eight-tick octave (T7) for aligned sums, allowing periodic extensions to yield k*Z(w) and closing the interface between pattern windows and observable block sums. It touches the T5 J-uniqueness and T8 D=3 landmarks by enabling discrete measurement of phi-ladder quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.