firstBlockSum_eq_Z_on_cylinder
If a boolean stream lies in the cylinder of an 8-bit pattern window, its first aligned 8-tick block sum equals the integer weight Z counting the ones in that window. Measurement and pattern-layer researchers cite this when reducing aligned sums to window functionals under cylinder membership. The proof is a short tactic sequence that rewrites the block sum to the general first-sum operator and applies the parameterized cylinder lemma for n=8.
claimLet $w$ be a pattern of length 8 and let $s$ be a boolean stream. If $s$ belongs to the cylinder set of $w$, then the sum of the first aligned 8-tick block of $s$ equals the number of true entries in $w$.
background
Streams are infinite boolean sequences indexed by natural numbers. A pattern of length n is a finite assignment of booleans to the first n positions. The cylinder of such a pattern collects all streams whose initial segment exactly matches the pattern. Z_of_window extracts the integer count of true bits inside the pattern. Sub-block sums extract the total over an aligned interval of length 8, the fundamental octave period.
proof idea
The tactic first unfolds the definition of the sub-block sum at offset 0 into the general first-sum operator, then simplifies the resulting arithmetic using the zero-addition and zero-multiplication lemmas. It finishes by invoking the general sum-first equality on cylinders, specialized to length 8.
why it matters in Recognition Science
The lemma is invoked by the Measurement layer's first-block equality and by the block-sum alias in the same module. It realizes the eight-tick octave (T7) by equating aligned block sums on cylinder streams to the window functional Z, closing the discrete measurement link between patterns and observable sums in the Recognition framework.
scope and limits
- Does not address sums over non-initial or misaligned blocks.
- Does not apply to windows whose length differs from 8 without the general lemma.
- Does not treat continuous time or non-boolean streams.
- Does not assert existence of streams outside the cylinder definition.
Lean usage
lemma blockSum_equals_Z_on_cylinder_first (w : Pattern 8) {s : Stream} (hs : s ∈ PatternLayer.Cylinder w) : blockSumAligned8 1 s = Z_of_window w := by classical; simp [blockSumAligned8, firstBlockSum_eq_Z_on_cylinder w (s:=s) hs]formal statement (Lean)
80lemma firstBlockSum_eq_Z_on_cylinder (w : Pattern 8) {s : Stream}
81 (hs : s ∈ PatternLayer.Cylinder w) :
82 subBlockSum8 s 0 = Z_of_window w := by
proof body
Tactic-mode proof.
83 classical
84 have hsum : subBlockSum8 s 0 = PatternLayer.sumFirst 8 s := by
85 unfold subBlockSum8 PatternLayer.sumFirst
86 simp [Nat.zero_mul, zero_add]
87 simpa [hsum] using
88 (PatternLayer.sumFirst_eq_Z_on_cylinder (n:=8) w (s:=s) hs)
89
90/-- Alias (T=8k, first block): if `s` is in the cylinder of `w`, then the
91 aligned block sum over the first 8‑tick block equals `Z(w)`. -/