synchronization_selection_principle

proof body

Tactic-mode proof.

  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) :=
 102          Nat.pow_lt_pow_right (by decide : 1 < (2 : Nat)) hlt
 103        have h3 : syncPeriod 3 = (2 ^ 3) * 45 := syncPeriod_eq_mul 3
 104        have hD' : syncPeriod (3 + Nat.succ k) = (2 ^ (3 + Nat.succ k)) * 45 :=
 105          syncPeriod_eq_mul (3 + Nat.succ k)
 106        have hmul : syncPeriod 3 < syncPeriod (3 + Nat.succ k) := by
 107          -- multiply strict inequality by 45 > 0 (again using commutativity)
 108          have : 45 * (2 ^ 3) < 45 * (2 ^ (3 + Nat.succ k)) :=
 109            (Nat.mul_lt_mul_left (by decide : 0 < 45)).2 hpowlt
 110          -- rewrite back to the paper order `(2^D)*45`
 111          have : (2 ^ 3) * 45 < (2 ^ (3 + Nat.succ k)) * 45 := by
 112            simpa [Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc] using this
 113          simpa [h3, hD'] using this
 114        -- contradiction: strict inequality implies not-equal
 115        exfalso
 116        exact (Nat.ne_of_lt hmul) (heq.symm)
 117
 118/-! A convenience corollary matching the paper's explicit numeric claim `lcm(8,45)=360`. -/