DriveSchedule

formal source

  25  deriving Repr
  26
  27/-- A drive schedule is a tick-indexed control stream. -/
  28abbrev DriveSchedule := ℕ → Control
  29
  30/-- Re-export: 8-gate neutrality predicate. -/
  31abbrev eightGateNeutral := SpiralField.eightGateNeutral
  32
  33/-- Re-export: 8-gate neutrality score (diagnostic). -/
  34abbrev neutralityScore := SpiralField.neutralityScore
  35
  36/-- Shift lemma for the neutrality score: shifting the start index shifts the sampled window. -/
  37lemma neutralityScore_succ (w : ℕ → ℝ) (t0 : ℕ) :
  38    neutralityScore w (t0 + 1) = (Finset.range 8).sum (fun k => w (t0 + 1 + k)) := by
  39  rfl
  40
  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`.