sum8
plain-language theorem explainer
sum8 computes the sum of eight consecutive values of a real-valued sequence over the natural numbers starting at t0. It is cited by work on neutrality predicates for periodic oscillators and spectral coherence diagnostics in Recognition Science. The definition is a direct one-line Finset summation using the period8 constant.
Claim. For a function $x : T → ℝ$ and $t_0 ∈ T$ where $T = ℕ$, define $∑_8(x, t_0) := ∑_{k=0}^{7} x(t_0 + k)$.
background
In the Breath1024 module, T is the abbreviation for the natural numbers, introduced as the domain for fundamental periods. period8 is the constant 8, implementing the eight-tick octave. The local setting concerns sliding-window sums that support neutrality checks for oscillators assumed to be period-8 and period-1024 periodic.
proof idea
This is a one-line wrapper that applies Finset.range sum over the period8 constant to the shifted sequence values.
why it matters
sum8 supplies the computational core for the neutral8 predicate that checks eight-window neutrality. It is reused directly in Nuclear.Octave for the isClosure magic-number predicate and in Spectra.SpectralLadder for eightGateCoherent coherence checks. The construction realizes the eight-tick octave (T7) step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.