IndisputableMonolith.Gap45

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Gap45
   5
   6open Nat
   7
   8/-- 9 and 5 are coprime. -/
   9@[simp] lemma coprime_9_5 : Nat.Coprime 9 5 := by decide
  10
  11/-- 8 and 45 are coprime. -/
  12@[simp] lemma coprime_8_45 : Nat.Coprime 8 45 := by decide
  13
  14/-- gcd(8,45) = 1. -/
  15@[simp] lemma gcd_8_45_eq_one : Nat.gcd 8 45 = 1 := by decide
  16
  17/-- lcm(8,45) = 360. -/
  18lemma lcm_8_45_eq_360 : Nat.lcm 8 45 = 360 := by
  19  have hg : Nat.gcd 8 45 = 1 := by decide
  20  have h := Nat.gcd_mul_lcm 8 45
  21  have : Nat.lcm 8 45 = 8 * 45 := by simpa [hg, Nat.one_mul] using h
  22  have hm : 8 * 45 = 360 := by decide
  23  exact this.trans hm
  24
  25/-- Exact cycle counts: lcm(8,45)/8 = 45. -/
  26lemma lcm_8_45_div_8 : Nat.lcm 8 45 / 8 = 45 := by
  27  have h := lcm_8_45_eq_360
  28  have : 360 / 8 = 45 := by decide
  29  simpa [h] using this
  30
  31/-- Exact cycle counts: lcm(8,45)/45 = 8. -/
  32lemma lcm_8_45_div_45 : Nat.lcm 8 45 / 45 = 8 := by
  33  have h := lcm_8_45_eq_360
  34  have : 360 / 45 = 8 := by decide
  35  simpa [h] using this
  36
  37/-- lcm(9,5) = 45, characterizing the first simultaneous occurrence of 9- and 5-fold periodicities. -/
  38lemma lcm_9_5_eq_45 : Nat.lcm 9 5 = 45 := by
  39  have hg : Nat.gcd 9 5 = 1 := by decide
  40  have h := Nat.gcd_mul_lcm 9 5
  41  have h' : Nat.lcm 9 5 = 9 * 5 := by simpa [hg, Nat.one_mul] using h
  42  have hmul : 9 * 5 = 45 := by decide
  43  simpa [hmul] using h'
  44
  45/-- 9 ∣ 45. -/
  46@[simp] lemma nine_dvd_45 : 9 ∣ 45 := by exact ⟨5, by decide⟩
  47
  48/-- 5 ∣ 45. -/
  49@[simp] lemma five_dvd_45 : 5 ∣ 45 := by exact ⟨9, by decide⟩
  50
  51/-- 8 ∤ 45. -/
  52@[simp] lemma eight_not_dvd_45 : ¬ 8 ∣ 45 := by decide
  53
  54/-- No positive `n < 45` is simultaneously divisible by 9 and 5. -/
  55lemma no_smaller_multiple_9_5 (n : Nat) (hnpos : 0 < n) (hnlt : n < 45) :
  56  ¬ (9 ∣ n ∧ 5 ∣ n) := by
  57  intro h
  58  rcases h with ⟨h9, h5⟩
  59  have hmul : 9 * 5 ∣ n := coprime_9_5.mul_dvd_of_dvd_of_dvd h9 h5
  60  have h45 : 45 ∣ n := by simpa using hmul
  61  rcases h45 with ⟨k, hk⟩
  62  rcases (Nat.eq_zero_or_pos k) with rfl | hkpos
  63  · simp only [mul_zero] at hk
  64    omega
  65  · have : 45 ≤ 45 * k := Nat.mul_le_mul_left 45 hkpos
  66    have : 45 ≤ n := by simpa [hk] using this
  67    exact (not_le_of_gt hnlt) this
  68
  69/-- Summary: 45 is the first rung where 9- and 5-fold periodicities coincide, and it is not
  70    synchronized with the 8-beat (since 8 ∤ 45). -/
  71theorem rung45_first_conflict :
  72  (9 ∣ 45) ∧ (5 ∣ 45) ∧ ¬ 8 ∣ 45 ∧ ∀ n, 0 < n → n < 45 → ¬ (9 ∣ n ∧ 5 ∣ n) := by
  73  refine ⟨nine_dvd_45, five_dvd_45, eight_not_dvd_45, ?_⟩
  74  intro n hnpos hnlt; exact no_smaller_multiple_9_5 n hnpos hnlt
  75
  76/-- Synchronization requirement: the minimal time to jointly align 8-beat and 45-fold symmetries
  77    is exactly lcm(8,45) = 360 beats, corresponding to 45 cycles of 8 and 8 cycles of 45. -/
  78theorem sync_counts :
  79  Nat.lcm 8 45 = 360 ∧ Nat.lcm 8 45 / 8 = 45 ∧ Nat.lcm 8 45 / 45 = 8 := by
  80  exact ⟨lcm_8_45_eq_360, lcm_8_45_div_8, lcm_8_45_div_45⟩
  81
  82/-- The beat-level clock-lag fraction implied by the 45-gap arithmetic: δ_time = 45/960 = 3/64. -/
  83theorem delta_time_eq_3_div_64 : (45 : ℚ) / 960 = (3 : ℚ) / 64 := by
  84  norm_num
  85
  86/-! ## Beat-level API (arithmetic mapping to 8-beat cycles). -/
  87namespace Beat
  88
  89/-- Minimal joint duration (in beats) for 8-beat and 45-fold patterns. -/
  90@[simp] def beats : Nat := Nat.lcm 8 45
  91
  92@[simp] lemma beats_eq_360 : beats = 360 := by
  93  simp [beats, lcm_8_45_eq_360]
  94
  95/-- Number of 8-beat cycles inside the minimal joint duration. -/
  96@[simp] lemma cycles_of_8 : beats / 8 = 45 := by
  97  simp [beats, lcm_8_45_div_8]
  98
  99/-- Number of 45-fold cycles inside the minimal joint duration. -/
 100@[simp] lemma cycles_of_45 : beats / 45 = 8 := by
 101  simp [beats, lcm_8_45_div_45]
 102
 103/-- Minimality: any time `t` that is simultaneously a multiple of 8 and 45 must be a
 104multiple of the minimal joint duration `beats` (i.e., 360). -/
 105lemma minimal_sync_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : beats ∣ t := by
 106  simpa [beats] using Nat.lcm_dvd h8 h45
 107
 108/-- Convenience form of minimality with 360 on the left. -/
 109lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
 110  simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
 111
 112/-- No positive `n < 360` can be simultaneously divisible by 8 and 45. -/
 113lemma no_smaller_multiple_8_45 {n : Nat} (hnpos : 0 < n) (hnlt : n < 360) :
 114  ¬ (8 ∣ n ∧ 45 ∣ n) := by
 115  intro h
 116  rcases h with ⟨h8, h45⟩
 117  have h360 : 360 ∣ n := minimal_sync_360_divides (t:=n) h8 h45
 118  rcases h360 with ⟨k, hk⟩
 119  rcases Nat.eq_zero_or_pos k with rfl | hkpos
 120  · simp only [mul_zero] at hk
 121    omega
 122  · have : 360 ≤ 360 * k := Nat.mul_le_mul_left 360 hkpos
 123    have : 360 ≤ n := by simpa [hk] using this
 124    exact (not_le_of_gt hnlt) this
 125
 126end Beat
 127
 128-- (Moved to IndisputableMonolith/Gap45/TimeLag.lean)
 129
 130-- (Moved to IndisputableMonolith/Gap45/RecognitionBarrier.lean)
 131
 132-- (Moved to IndisputableMonolith/Gap45/GroupView.lean)
 133
 134-- (Moved to IndisputableMonolith/Gap45/AddGroupView.lean)
 135
 136end Gap45
 137end IndisputableMonolith
 138