sumFirst
sumFirst counts the number of true bits in the initial segment of length m of a boolean stream s. Workers on periodic stream extensions and cylinder sets cite it to reduce finite window sums to the Z invariant. The definition is a direct summation over Fin m using an indicator on each stream value.
claimLet $m$ be a natural number and let $s : {0,1,2,ldots} to {true,false}$ be a stream. Define $sumFirst(m,s) := sum_{i=0}^{m-1} 1_{s(i)}$, where $1_{s(i)}$ equals 1 if $s(i)$ is true and 0 otherwise.
background
A Stream is a function from natural numbers to booleans, serving as an infinite bit sequence. The Streams module develops periodic extensions of finite patterns together with finite initial sums. Upstream structures supply the J-cost calibration and the spectral emergence of gauge groups and generations, providing the broader Recognition Science setting in which these stream operations appear.
proof idea
The declaration is a direct definition that unfolds to summation over the finite index set Fin m. Each term is obtained by the indicator (if s i.val then 1 else 0). No auxiliary lemmas are invoked; the expression itself is the primitive operation used by later results.
why it matters in Recognition Science
This definition supplies the base operation for lemmas such as sumFirst_eq_Z_on_cylinder and sumFirst8_extendPeriodic_eq_Z that equate initial sums to the Z_of_window invariant on patterns. It supports the eight-tick octave by enabling sums over length-8 periodic extensions and feeds directly into Measurement.sumFirst and the Blocks module. The construction aligns with the T7 eight-tick structure in the forcing chain.
scope and limits
- Does not sum over an infinite stream or tail.
- Does not assume or enforce periodicity of s.
- Does not incorporate J-cost, phi-ladder, or mass formulas.
- Does not handle real-valued or continuous streams.
Lean usage
sumFirst 8 (extendPeriodic8 w) = Z_of_window wformal statement (Lean)
68def sumFirst (m : Nat) (s : Stream) : Nat :=
proof body
Definition body.
69 ∑ i : Fin m, (if s i.val then 1 else 0)
70
71/-- Base case: the sum of the first 0 bits is 0. -/