IndisputableMonolith.Flight.Schedule

   1import Mathlib
   2import IndisputableMonolith.Spiral.SpiralField
   3
   4/-!
   5# Flight Scheduling (8-tick control discipline)
   6
   7This file defines a minimal control/schedule surface and reuses the existing
   88-window neutrality predicates from `SpiralField`.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Flight
  13namespace Schedule
  14
  15open scoped BigOperators
  16
  17open IndisputableMonolith.Spiral
  18
  19/-- Minimal control datum per tick.
  20
  21This is intentionally small; hardware-level specs will refine this later.
  22-/
  23structure Control where
  24  pulse : Bool
  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`.
  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. -/
  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
 114