syncPeriod

formal source

  52open Nat
  53
  54/-- The synchronization period used in `Draft_v1.tex`: `S(D) := lcm(2^D, 45)`. -/
  55def syncPeriod (D : ℕ) : ℕ := Nat.lcm (2 ^ D) 45
  56
  57lemma syncPeriod_def (D : ℕ) : syncPeriod D = Nat.lcm (2 ^ D) 45 := rfl
  58
  59/-! The key arithmetic lemma used in the paper's proof: since `45` is odd,
  60`gcd(2^D,45)=1`, hence `lcm(2^D,45)=2^D*45`. -/
  61theorem syncPeriod_eq_mul (D : ℕ) : syncPeriod D = (2 ^ D) * 45 := by
  62  unfold syncPeriod
  63  have h2 : Nat.Coprime 2 45 := by decide
  64  have h : Nat.Coprime (2 ^ D) 45 := h2.pow_left D
  65  simpa using h.lcm_eq_mul
  66
  67/-! ### Synchronization Selection Principle (proved) -/
  68
  69/-- A direct formalization of the paper's minimization statement:
  70among all `D ≥ 3`, the function `D ↦ lcm(2^D,45)` is minimized uniquely at `D = 3`. -/
  71theorem synchronization_selection_principle {D : ℕ} (hD : 3 ≤ D) :
  72    syncPeriod 3 ≤ syncPeriod D ∧ (syncPeriod D = syncPeriod 3 → D = 3) := by
  73  constructor
  74  · -- monotonicity from the closed form
  75    have h3 : syncPeriod 3 = (2 ^ 3) * 45 := syncPeriod_eq_mul 3
  76    have hD' : syncPeriod D = (2 ^ D) * 45 := syncPeriod_eq_mul D
  77    -- show 2^3 ≤ 2^D using D = 3 + k
  78    rcases Nat.exists_eq_add_of_le hD with ⟨k, rfl⟩
  79    have hk : 1 ≤ 2 ^ k := Nat.one_le_pow k 2 (by norm_num)
  80    have hpow : 2 ^ 3 ≤ 2 ^ (3 + k) := by
  81      calc
  82        2 ^ 3 = 2 ^ 3 * 1 := by ring
  83        _ ≤ 2 ^ 3 * 2 ^ k := by exact Nat.mul_le_mul_left (2 ^ 3) hk
  84        _ = 2 ^ (3 + k) := by
  85          -- 2^(3+k) = 2^3 * 2^k