apsidalAngle

formal source

 145
 146/-- The apsidal-angle formula used in `Draft_v1.tex` after substituting the Green-kernel power
 147law: `Δθ(D) = 2π / √(4 - D)` (with `D` treated as a real parameter). -/
 148noncomputable def apsidalAngle (D : ℕ) : ℝ :=
 149  (2 * Real.pi) / Real.sqrt (4 - (D : ℝ))
 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