sumFirst_eq_Z_on_cylinder
A stream agreeing with a finite pattern on its initial n bits has its partial sum equal to the window's one-count Z. Pattern-matching arguments in the measurement layer cite this to equate cylinder membership with integer functionals. The tactic proof unfolds the three definitions, applies functional extensionality to the indicator functions, and simplifies using the cylinder hypothesis.
claimLet $w$ be a pattern of length $n$ and let $s$ be a stream lying in the cylinder set of $w$. Then the sum of the first $n$ bits of $s$ equals the integer $Z$ of the window $w$.
background
Pattern is the type of finite Boolean sequences of length $n$. Stream is the type of infinite Boolean sequences. Cylinder w is the set of all streams that match w exactly on the first $n$ positions. Z_of_window w is the sum over i in Fin n of the indicator (1 if w i is true). sumFirst n s is the analogous sum of the first n bits of s.
proof idea
The proof unfolds sumFirst, Z_of_window and Cylinder. It then proves the two indicator functions on Fin n are identical by funext and simp using the membership hypothesis hs at each i. A final simp closes the equality of the two Nat sums.
why it matters in Recognition Science
The lemma is invoked directly by firstBlockSum_eq_Z_on_cylinder in Streams.Blocks, which specializes the result to 8-bit windows under periodic extension. It supplies the basic interface between cylinder membership and the integer Z used in anchor and mass calculations, supporting the eight-tick octave structure of the Recognition framework.
scope and limits
- Does not equate sums that begin at arbitrary offsets.
- Does not address convergence of infinite sums.
- Does not claim that every stream belongs to a unique cylinder.
formal statement (Lean)
76lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
77 {s : Stream} (hs : s ∈ Cylinder w) :
78 sumFirst n s = Z_of_window w := by
proof body
Tactic-mode proof.
79 unfold sumFirst Z_of_window Cylinder at *
80 have : (fun i : Fin n => (if s i.val then 1 else 0)) =
81 (fun i : Fin n => (if w i then 1 else 0)) := by
82 funext i; simp [hs i]
83 simp [this]
84
85/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/