eightGateNeutral_shift_invariance
plain-language theorem explainer
A signal periodic with period 8 has its 8-gate neutrality invariant under a one-tick shift of the reference time. Flight scheduling arguments cite this to relocate the observation window while preserving the zero-sum condition. The proof reduces the biconditional to the shift equality for the neutrality score via unfolding and simplification.
Claim. Let $w : ℕ → ℝ$ satisfy $w(t+8)=w(t)$ for all $t$. Then $∑_{k=0}^7 w(t_0 + k) = 0$ if and only if $∑_{k=0}^7 w(t_0 + 1 + k) = 0$.
background
The Flight module supplies an 8-tick control surface that re-exports neutrality predicates from SpiralField. Periodic8 is the predicate asserting $w(t+8)=w(t)$ for every natural number $t$. eightGateNeutral requires the sum of any eight consecutive values of $w$ to vanish; neutralityScore records the numerical value of that sum. The upstream lemma neutralityScore_shift1_of_periodic8 states that the score itself is unchanged by a unit shift whenever Periodic8 holds.
proof idea
The tactic proof unfolds eightGateNeutral and neutralityScore, then splits the biconditional with constructor. Each direction applies neutralityScore_shift1_of_periodic8 to equate the two scores, after which simpa transfers the zero condition.
why it matters
The result supplies shift invariance inside the 8-tick control discipline and is referenced by the FlightReport summary. It realizes the T7 eight-tick octave of the forcing chain, guaranteeing that neutrality conditions remain stable under discrete time shifts within periodic schedules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.