eightGateNeutral_shift_invariance
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish periodicity for any signal.
- Does not apply when the Periodic8 hypothesis is dropped.
- Does not compute explicit numerical values of the sum.
- Does not extend to periods other than 8.
- Does not treat continuous-time signals.
formal statement (Lean)
91theorem eightGateNeutral_shift_invariance (w : ℕ → ℝ) (t0 : ℕ) (hper : Periodic8 w) :
92 eightGateNeutral w t0 ↔ eightGateNeutral w (t0 + 1) := by
proof body
Tactic-mode proof.
93 unfold eightGateNeutral SpiralField.eightGateNeutral
94 constructor <;> intro h
95 · -- forward direction
96 have hs : neutralityScore w (t0 + 1) = neutralityScore w t0 :=
97 neutralityScore_shift1_of_periodic8 w t0 hper
98 have h0 : neutralityScore w t0 = 0 := by
99 simpa [SpiralField.neutralityScore] using h
100 have : neutralityScore w (t0 + 1) = 0 := by simpa [hs] using h0
101 simpa [SpiralField.neutralityScore] using this
102 · -- backward direction (symmetry)
103 have hs : neutralityScore w (t0 + 1) = neutralityScore w t0 :=
104 neutralityScore_shift1_of_periodic8 w t0 hper
105 have h1 : neutralityScore w (t0 + 1) = 0 := by
106 simpa [SpiralField.neutralityScore] using h
107 have : neutralityScore w t0 = 0 := by simpa [hs] using h1
108 simpa [SpiralField.neutralityScore] using this
109
110end Schedule
111end Flight
112end IndisputableMonolith
113