scheduleNeutral

formal source

  80abbrev Schedule := Fin 8 → ℤ
  81
  82/-- The neutrality constraint: sum over any aligned 8-tick window is zero. -/
  83def scheduleNeutral (s : Schedule) : Prop := (∑ i : Fin 8, s i) = 0
  84
  85/-- A neutral schedule with half positive and half negative is achievable. -/
  86def balancedSchedule : Schedule :=
  87  fun i => if i.val < 4 then 1 else -1
  88
  89theorem balancedSchedule_neutral : scheduleNeutral balancedSchedule := by
  90  unfold scheduleNeutral balancedSchedule
  91  simp [Fin.sum_univ_eight]
  92
  93/-! ## Safety Requirements -/
  94
  95/-- Nautilus safety requirements (from NTL-008/018). -/
  96structure SafetyRequirements where
  97  has_watchdog : Bool
  98  has_overcurrent_protection : Bool
  99  has_overvoltage_protection : Bool
 100  has_thermal_protection : Bool
 101  has_loss_of_load_detection : Bool
 102  has_deterministic_shutdown : Bool
 103  all_satisfied :
 104    has_watchdog = true ∧
 105    has_overcurrent_protection = true ∧
 106    has_overvoltage_protection = true ∧
 107    has_thermal_protection = true ∧
 108    has_loss_of_load_detection = true ∧
 109    has_deterministic_shutdown = true
 110
 111/-- The canonical safety configuration. -/
 112def fullSafety : SafetyRequirements where
 113  has_watchdog := true