sum8
plain-language theorem explainer
sum8 delivers a sliding sum of eight consecutive real values from a sequence indexed by naturals, starting at t0. Spectral coherence work in Recognition Science cites it for eight-window neutrality diagnostics on rails. The definition is a direct Finset.range summation over the eight offsets.
Claim. Let $s(x, t_0) = sum_{k=0}^{7} x(t_0 + k)$ for a map $x : ℕ → ℝ$.
background
The SpectralLadder module scaffolds cross-domain spectral rails with frequencies scaling as f_n = f0 · φ^{2n}. sum8 supplies the basic eight-sample sliding sum used for coherence and neutrality diagnostics. Upstream, Breath1024 defines an analogous eight-window sum as an eight-window neutrality predicate, while Nuclear.Octave uses the same form for closure checks.
proof idea
This is a one-line definition that applies Finset.range 8 to sum the shifted sequence values x(t0 + k).
why it matters
The definition supports neutral8 in Breath1024, isClosure in Nuclear.Octave, and eightGateCoherent locally. It instantiates the eight-tick octave (T7) for spectral applications. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.