IndisputableMonolith.Gap45.Beat

   1import Mathlib
   2import IndisputableMonolith.Measurement
   3
   4namespace IndisputableMonolith
   5namespace Gap45
   6
   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
  41
  42lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
  43  simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
  44
  45lemma no_smaller_multiple_8_45 {n : Nat} (hnpos : 0 < n) (hnlt : n < 360) :
  46  ¬ (8 ∣ n ∧ 45 ∣ n) := by
  47  intro h; rcases h with ⟨h8, h45⟩
  48  have h360 : 360 ∣ n := minimal_sync_360_divides (t:=n) h8 h45
  49  rcases h360 with ⟨k, hk⟩
  50  rcases Nat.eq_zero_or_pos k with rfl | hkpos
  51  · -- k = 0, so n = 360 * 0 = 0, contradicting hnpos : 0 < n
  52    simp only [Nat.mul_zero] at hk
  53    omega
  54  · have : 360 ≤ 360 * k := Nat.mul_le_mul_left 360 hkpos
  55    have : 360 ≤ n := by simpa [hk] using this
  56    exact (not_le_of_gt hnlt) this
  57
  58structure Sync where
  59  beats : Nat
  60  cycles8 : beats / 8 = 45
  61  cycles45 : beats / 45 = 8
  62
  63noncomputable def canonical : Sync :=
  64  { beats := beats
  65  , cycles8 := cycles_of_8
  66  , cycles45 := cycles_of_45 }
  67
  68end Beat
  69
  70namespace TimeLag
  71
  72@[simp] lemma lag_q : (45 : ℚ) / ((8 : ℚ) * (120 : ℚ)) = (3 : ℚ) / 64 := by
  73  norm_num
  74
  75@[simp] lemma lag_r : (45 : ℝ) / ((8 : ℝ) * (120 : ℝ)) = (3 : ℝ) / 64 := by
  76  norm_num
  77
  78end TimeLag
  79
  80end Gap45
  81end IndisputableMonolith
  82