synchronization_selection_principle

formal source

  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
  86          simp [Nat.pow_add]
  87    -- multiply by 45 on the right (commuting as needed)
  88    have hmul : (2 ^ 3) * 45 ≤ (2 ^ (3 + k)) * 45 := by
  89      -- use commutativity so we can multiply on the left
  90      have : 45 * (2 ^ 3) ≤ 45 * (2 ^ (3 + k)) := Nat.mul_le_mul_left 45 hpow
  91      simpa [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using this
  92    simpa [h3, hD', Nat.add_assoc] using hmul
  93  · intro heq
  94    -- use strictness: if D>3 then syncPeriod 3 < syncPeriod D, contradiction
  95    rcases Nat.exists_eq_add_of_le hD with ⟨k, rfl⟩
  96    cases k with
  97    | zero =>
  98        simp
  99    | succ k =>
 100        have hlt : 3 < 3 + Nat.succ k := Nat.lt_add_of_pos_right (by exact Nat.succ_pos _)
 101        have hpowlt : 2 ^ 3 < 2 ^ (3 + Nat.succ k) :=