kepler_selection_principle

formal source

 150
 151/-- A direct formalization of the paper's last step:
 152`Δθ = 2π` holds iff `D=3` for the substituted closed-form apsidal angle. -/
 153theorem kepler_selection_principle (D : ℕ) :
 154    apsidalAngle D = 2 * Real.pi ↔ D = 3 := by
 155  constructor
 156  · intro h
 157    have hpi : (2 * Real.pi) ≠ 0 := by
 158      exact mul_ne_zero (by norm_num) Real.pi_ne_zero
 159    -- Let x be the denominator √(4 - D).
 160    set x : ℝ := Real.sqrt (4 - (D : ℝ))
 161    have hx : x ≠ 0 := by
 162      intro hx0
 163      have : apsidalAngle D = 0 := by
 164        simp [apsidalAngle, x, hx0]
 165      have h0 : 0 = 2 * Real.pi := by
 166        simpa [this] using h
 167      exact hpi h0.symm
 168    -- Rewrite h as (2π) * x⁻¹ = 2π, then cancel.
 169    have h' : (2 * Real.pi) * x⁻¹ = 2 * Real.pi := by
 170      simpa [apsidalAngle, x, div_eq_mul_inv] using h
 171    have hmul : (2 * Real.pi) * (x⁻¹ * x) = (2 * Real.pi) * x := by
 172      -- multiply both sides by x
 173      simpa [mul_assoc] using congrArg (fun t => t * x) h'
 174    have hmul' : (2 * Real.pi) = (2 * Real.pi) * x := by
 175      simpa [mul_assoc, inv_mul_cancel₀ hx, mul_one] using hmul
 176    -- cancel 2π to get x = 1
 177    have hx1 : x = 1 := by
 178      have hcancel : (2 * Real.pi) * x = (2 * Real.pi) * 1 := by
 179        calc
 180          (2 * Real.pi) * x = (2 * Real.pi) := by simpa [mul_assoc] using hmul'.symm
 181          _ = (2 * Real.pi) * 1 := by simp
 182      exact mul_left_cancel₀ hpi hcancel
 183    -- show 0 ≤ 4 - D so we can square the sqrt