eightGateNeutral_shift_invariance

formal source

  88    _ = (Finset.range 8).sum (fun k => w (t0 + k)) := hR
  89
  90/-- Main schedule-shift invariant: if the signal is 8-periodic, the 8-gate sum is invariant under a shift. -/
  91theorem eightGateNeutral_shift_invariance (w : ℕ → ℝ) (t0 : ℕ) (hper : Periodic8 w) :
  92    eightGateNeutral w t0 ↔ eightGateNeutral w (t0 + 1) := by
  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