neutralityScore_shift1_of_periodic8

proof body

Tactic-mode proof.

  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        =
  75        (Finset.range 7).sum (fun k => w (t0 + (k + 1))) := by
  76    refine Finset.sum_congr rfl ?_
  77    intro k hk
  78    simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
  79
  80  -- Put it together.
  81  calc
  82    (Finset.range 8).sum (fun k => w (t0 + 1 + k))
  83        = (Finset.range 7).sum (fun k => w (t0 + 1 + k)) + w (t0 + 8) := hL
  84    _ = (Finset.range 7).sum (fun k => w (t0 + (k + 1))) + w t0 := by
  85          simp [hsum7, hw8]
  86    _ = (Finset.range 7).sum (fun k => w (t0 + (k + 1))) + w (t0 + 0) := by
  87          simp
  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. -/