neutral8
plain-language theorem explainer
The neutral8 definition computes the sum of eight consecutive terms from a real-valued sequence on the naturals, beginning at a specified index. Chemists and modelers using Recognition Science for environment-rescaled observables would cite it when performing neutrality diagnostics over the eight-tick window. It supports fixing the exponent β in the pressure rescale while leaving integer scaffolding unchanged. The implementation is a direct finite summation with no further lemmas or reductions.
Claim. For a function $x : ℕ → ℝ$ and starting index $t_0 ∈ ℕ$, the eight-term sum is defined by $∑_{i=0}^{7} x(t_0 + i)$.
background
The EnvPressure module provides display-only rescales for environment-dependent observables via the map $E ↦ E · φ^{β P}$, with β fixed by neutrality tests and integer scaffolding left intact. This definition supplies an eight-term summation helper aligned with the period-8 octave. Upstream results include the analogous summation in SelectionRules, documented as counting legal triads in a finite list, and the zero-sum check in Breath1024 for generative and radiative oscillator streams assumed period-8 and period-1024 periodic.
proof idea
The definition is a direct one-line wrapper that applies the Finset.range 8 summation operator to the sequence shifted by t0. No tactics or lemmas are invoked beyond the standard Mathlib finite-sum construction.
why it matters
This helper enables the neutrality tests that determine β for the environment rescale, feeding directly into the neutral8 summation used in crystallography selection rules and the zero-sum oscillator record in the breath foundation. It touches the eight-tick octave step of the forcing chain and supports closure of display-level scaffolding for chemistry observables without altering core Recognition Science structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.