IndisputableMonolith.Verification.DimensionKepler

   1import Mathlib
   2
   3/-!
   4# Kepler Specialization for Dimension Selection
   5
   6This module isolates the algebraic core used by the `(K)` specialization in the
   7dimensional rigidity paper:
   8
   9* define the closed-form apsidal-angle expression
  10  `Δθ(D) = 2π / √(4 - D)`;
  11* prove `Δθ(D) = 2π ↔ D = 3`.
  12
  13This is intentionally the reduced-form endpoint theorem (after the classical
  14mechanics derivation), so it can be referenced from the verification layer.
  15-/
  16
  17noncomputable section
  18
  19namespace IndisputableMonolith
  20namespace Verification
  21namespace DimensionKepler
  22
  23open Real
  24
  25/-- Closed-form apsidal angle used in the Kepler specialization. -/
  26noncomputable def apsidalAngle (D : ℕ) : ℝ :=
  27  (2 * Real.pi) / Real.sqrt (4 - (D : ℝ))
  28
  29/-- Algebraic Kepler selector: `Δθ = 2π` holds exactly at `D = 3`. -/
  30theorem kepler_selection_principle (D : ℕ) :
  31    apsidalAngle D = 2 * Real.pi ↔ D = 3 := by
  32  constructor
  33  · intro h
  34    have hpi : (2 * Real.pi) ≠ 0 := by
  35      exact mul_ne_zero (by norm_num) Real.pi_ne_zero
  36    set x : ℝ := Real.sqrt (4 - (D : ℝ))
  37    have hx : x ≠ 0 := by
  38      intro hx0
  39      have : apsidalAngle D = 0 := by
  40        simp [apsidalAngle, x, hx0]
  41      have h0 : 0 = 2 * Real.pi := by
  42        simpa [this] using h
  43      exact hpi h0.symm
  44    have h' : (2 * Real.pi) * x⁻¹ = 2 * Real.pi := by
  45      simpa [apsidalAngle, x, div_eq_mul_inv] using h
  46    have hmul : (2 * Real.pi) * (x⁻¹ * x) = (2 * Real.pi) * x := by
  47      simpa [mul_assoc] using congrArg (fun t => t * x) h'
  48    have hmul' : (2 * Real.pi) = (2 * Real.pi) * x := by
  49      simpa [mul_assoc, inv_mul_cancel₀ hx, mul_one] using hmul
  50    have hx1 : x = 1 := by
  51      have hcancel : (2 * Real.pi) * x = (2 * Real.pi) * 1 := by
  52        calc
  53          (2 * Real.pi) * x = (2 * Real.pi) := by simpa [mul_assoc] using hmul'.symm
  54          _ = (2 * Real.pi) * 1 := by simp
  55      exact mul_left_cancel₀ hpi hcancel
  56    have hnonneg : 0 ≤ 4 - (D : ℝ) := by
  57      by_contra hneg
  58      have hle : 4 - (D : ℝ) ≤ 0 := le_of_not_ge hneg
  59      have : Real.sqrt (4 - (D : ℝ)) = 0 := Real.sqrt_eq_zero_of_nonpos hle
  60      have : (1 : ℝ) = 0 := by simpa [x, hx1] using this
  61      exact one_ne_zero this
  62    have hsq : x ^ 2 = 4 - (D : ℝ) := by
  63      simpa [x, pow_two] using (Real.sq_sqrt hnonneg)
  64    have hreal : (D : ℝ) = 3 := by
  65      have : (1 : ℝ) ^ 2 = 4 - (D : ℝ) := by simpa [hx1] using hsq
  66      nlinarith
  67    exact (Nat.cast_injective (R := ℝ) (by simpa using hreal))
  68  · intro hD
  69    subst hD
  70    have : (4 - (3 : ℝ)) = (1 : ℝ) := by norm_num
  71    simp [apsidalAngle, this]
  72
  73end DimensionKepler
  74end Verification
  75end IndisputableMonolith
  76
  77