neutral8
plain-language theorem explainer
neutral8 defines the sum of eight consecutive real values drawn from a sequence w beginning at index i0. Crystallographers testing LNAL-inspired selection rules against space-group data would cite this for eight-window neutrality checks. The definition is a direct finite summation over the eight-element range.
Claim. Let $w : ℕ → ℝ$ and $i_0 ∈ ℕ$. The eight-window neutral sum is defined as $∑_{k=0}^{7} w(i_0 + k)$.
background
The Crystallography.SelectionRules module supplies LNAL-inspired predicates that translate eight-window neutrality and legal SU(3) triads into reciprocal-space motif constraints for empirical bias tests against space-group frequencies. The neutral8 definition supplies the basic summation operator over an eight-term window. It mirrors the identical summation appearing in the EnvPressure module and the zero-sum proposition used for period-8 oscillator records in the Breath1024 foundation module.
proof idea
The definition is a direct one-line construction that applies the Finset sum operator to the range of eight consecutive indices starting at i0.
why it matters
This definition supplies the neutrality window sum required by the selection-rules scaffold and is referenced by the EnvPressure and Breath1024 modules. It instantiates the eight-tick octave (T7) from the unified forcing chain for motif constraints. The module remains scaffolding for future empirical tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.