sumFirst_eq_Z_on_cylinder
Streams whose initial segment matches a finite pattern window have their prefix sum equal to the window's one-count Z. Measurement-layer proofs in the Recognition Science streams module cite this equality when aligning block sums to integer functionals. The tactic proof proceeds by classical unfolding of the definitions followed by a function extensionality step that equates the indicator functions pointwise.
claimIf a stream $s$ lies in the cylinder set generated by a pattern $w$ of length $n$, then the sum of the first $n$ bits of $s$ equals the integer $Z$ counting the ones in $w$.
background
Pattern $n$ is the type Fin $n$ → Bool for finite bit windows. Stream is the type Nat → Bool for infinite sequences. Cylinder $w$ is the set of streams whose first $n$ positions match $w$ exactly. Z_of_window $w$ is the sum over Fin $n$ of the indicator (1 if true, 0 otherwise), while sumFirst $n$ $s$ computes the same sum on the stream prefix.
proof idea
The tactic proof opens with classical, unfolds sumFirst, Z_of_window, and Cylinder, then uses funext to equate the two indicator functions pointwise from the cylinder membership hypothesis, after which simpa closes the goal.
why it matters in Recognition Science
This lemma is invoked by the re-exported sumFirst_eq_Z_on_cylinder in the parent Streams module and by firstBlockSum_eq_Z_on_cylinder for aligned 8-bit blocks. It supplies the direct reduction from stream prefixes to window integers, supporting measurement alignment with the eight-tick octave and phi-ladder mass formulas in the Recognition framework.
scope and limits
- Does not address sums at arbitrary offsets or non-prefix positions.
- Does not assume periodicity or restrict to n=8.
- Does not compute explicit numerical values of Z.
- Does not extend to infinite or convergent sums.
Lean usage
example {n : Nat} (w : Pattern n) (s : Stream) (hs : s ∈ Cylinder w) : sumFirst n s = Z_of_window w := sumFirst_eq_Z_on_cylinder w hsformal statement (Lean)
39lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
40 {s : Stream} (hs : s ∈ Cylinder w) :
41 sumFirst n s = Z_of_window w := by
proof body
Tactic-mode proof.
42 classical
43 unfold sumFirst Z_of_window Cylinder at *
44 have : (fun i : Fin n => (if s i.val then 1 else 0)) =
45 (fun i : Fin n => (if w i then 1 else 0)) := by
46 funext i; simpa [hs i]
47 simpa [this]
48
49/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/