requiresExperience

formal source

   7/-! Gap45 gating rule: experience is required exactly when the plan period is not
   8    a multiple of 8. This captures the Source.txt policy that 8-beat alignment
   9    disables Gap45 gating. -/
  10@[simp] def requiresExperience (_c : IndisputableMonolith.Measurement.CQ) (period : Nat) : Prop :=
  11  ¬ (8 ∣ period)
  12
  13@[simp] lemma gcd_8_45_eq_one : Nat.gcd 8 45 = 1 := by decide
  14
  15lemma lcm_8_45_eq_360 : Nat.lcm 8 45 = 360 := by
  16  decide
  17
  18lemma lcm_8_45_div_8 : Nat.lcm 8 45 / 8 = 45 := by
  19  have h := lcm_8_45_eq_360
  20  simpa [h]
  21
  22lemma lcm_8_45_div_45 : Nat.lcm 8 45 / 45 = 8 := by
  23  have h := lcm_8_45_eq_360
  24  simpa [h]
  25
  26namespace Beat
  27
  28@[simp] def beats : Nat := Nat.lcm 8 45
  29
  30@[simp] lemma beats_eq_360 : beats = 360 := by
  31  simp [beats, lcm_8_45_eq_360]
  32
  33@[simp] lemma cycles_of_8 : beats / 8 = 45 := by
  34  simp [beats, lcm_8_45_div_8]
  35
  36@[simp] lemma cycles_of_45 : beats / 45 = 8 := by
  37  simp [beats, lcm_8_45_div_45]
  38
  39lemma minimal_sync_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : beats ∣ t := by
  40  simpa [beats] using Nat.lcm_dvd h8 h45