subBlockSum8
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume or enforce periodicity of the stream.
- Does not sum over windows of length other than 8.
- Does not incorporate J-cost, phi-ladder, or physical constants.
- Does not handle non-aligned starting indices.
formal statement (Lean)
71def subBlockSum8 (s : Stream) (j : Nat) : Nat :=
proof body
Definition body.
72 ∑ i : Fin 8, (if s (j * 8 + i.val) then 1 else 0)
73
74/-- Aligned block sum over `k` copies of the 8‑tick window (so instrument length `T=8k`). -/