neutralityScore
plain-language theorem explainer
The neutrality score sums a weight function over eight consecutive natural numbers starting at a given index. Analysts of periodic eight-phase schedules in the Recognition framework cite this when establishing shift invariance. The definition is a direct finite sum with no additional lemmas required.
Claim. Let $w : ℕ → ℝ$ and $t_0 ∈ ℕ$. The neutrality score equals $∑_{k=0}^{7} w(t_0 + k)$.
background
The Spiral Wavefields module supplies a variational ansatz for logarithmic spiral fields under φ-scaling together with an eight-tick gating constraint. Only basic structures appear; no theorems are proved in the file. The neutrality score functions as the elementary diagnostic that adds weights across one full eight-tick window.
proof idea
This is a direct definition that expands to the standard sum over Finset.range 8 of the shifted weight values. No upstream lemmas are invoked beyond the built-in summation operator.
why it matters
The definition supplies the concrete sum used by eightGateNeutral_shift_invariance and neutralityScore_shift1_of_periodic8 in Flight.Schedule. Those results establish invariance of the eight-gate sum under unit shifts when the weight is 8-periodic, realizing the eight-tick octave (T7) inside the spiral-field ansatz. It therefore anchors the gating constraint that appears throughout the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.