neutralityScore_shift1_of_periodic8

formal source

  41/-- Simple 8-periodicity predicate (for “8-phase schedules”). -/
  42def Periodic8 (w : ℕ → ℝ) : Prop := ∀ t, w (t + 8) = w t
  43
  44lemma neutralityScore_shift1_of_periodic8 (w : ℕ → ℝ) (t0 : ℕ) (hper : Periodic8 w) :
  45    neutralityScore w (t0 + 1) = neutralityScore w t0 := by
  46  classical
  47  -- Expand both scores as sums over 8 consecutive ticks.
  48  unfold neutralityScore SpiralField.neutralityScore
  49  -- Use periodicity to rewrite the last term `w (t0+8)` into `w t0`.
  50  have hw8 : w (t0 + 8) = w t0 := by
  51    simpa [Periodic8, Nat.add_assoc] using hper t0
  52
  53  -- LHS: split off the last element (k=7), so we can rewrite it using periodicity.
  54  have hL :
  55      (Finset.range 8).sum (fun k => w (t0 + 1 + k))
  56        =
  57        (Finset.range 7).sum (fun k => w (t0 + 1 + k)) + w (t0 + 8) := by
  58    -- `sum_range_succ` peels off the last term at index `7`.
  59    simpa [Finset.sum_range_succ, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using
  60      (Finset.sum_range_succ (fun k => w (t0 + 1 + k)) 7)
  61
  62  -- RHS: peel off the *first* element (k=0) via `sum_range_succ'`.
  63  have hR :
  64      (Finset.range 7).sum (fun k => w (t0 + (k + 1))) + w (t0 + 0)
  65        =
  66        (Finset.range 8).sum (fun k => w (t0 + k)) := by
  67    -- `sum_range_succ'` states the reverse direction; we use `.symm`.
  68    simpa [Finset.sum_range_succ', Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using
  69      (Finset.sum_range_succ' (fun k => w (t0 + k)) 7).symm
  70
  71  -- Normalize the 7-term sums: `t0 + 1 + k = t0 + (k + 1)`.
  72  have hsum7 :
  73      (Finset.range 7).sum (fun k => w (t0 + 1 + k))
  74        =