IndisputableMonolith.Relativity.Compact.StaticSpherical

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry
   3import IndisputableMonolith.Relativity.Calculus
   4import IndisputableMonolith.Relativity.Fields
   5
   6namespace IndisputableMonolith
   7namespace Relativity
   8namespace Compact
   9
  10open Geometry
  11open Calculus
  12open Fields
  13
  14structure StaticSphericalMetric where
  15  f : ℝ → ℝ
  16  g : ℝ → ℝ
  17  f_positive : ∀ r, r > 0 → f r > 0
  18  g_positive : ∀ r, r > 0 → g r > 0
  19
  20structure StaticScalarField where
  21  psi : ℝ → ℝ
  22
  23-- Field equations would go here (complex ODEs)
  24/-!
  25Field equations (documentation / TODO).
  26
  27The static-spherical field equations (coupled ODE/PDE system) are not yet formalized in this module.
  28-/
  29
  30/-- **DEFINITION: Schwarzschild Metric**
  31    The static spherical solution for vacuum (M ≠ 0, ρ = 0, ψ = 0).
  32    f(r) = 1 - 2M/r, g(r) = (1 - 2M/r)⁻¹ for r > 2|M|.
  33    For r ≤ 2|M|, we use a positive constant to satisfy the metric structure
  34    outside the coordinate singularity. -/
  35noncomputable def SchwarzschildMetric (M : ℝ) : StaticSphericalMetric :=
  36  { f := fun r => if r > 2 * |M| then 1 - 2 * M / r else 1
  37    g := fun r => if r > 2 * |M| then 1 / (1 - 2 * M / r) else 1
  38    f_positive := by
  39      intro r hr
  40      by_cases h_rad : r > 2 * |M|
  41      · simp [h_rad]
  42        -- 1 - 2M/r > 0  ⟺  r > 2M
  43        -- We have r > 2|M| and 2|M| ≥ 2M
  44        have h_gt : r > 2 * M := by linarith [abs_le_abs_self M, le_abs_self M]
  45        apply sub_pos.mpr
  46        rw [div_lt_one hr]
  47        linarith
  48      · simp [h_rad]
  49        norm_num
  50    g_positive := by
  51      intro r hr
  52      by_cases h_rad : r > 2 * |M|
  53      · simp [h_rad]
  54        have h_gt : r > 2 * M := by linarith [abs_le_abs_self M, le_abs_self M]
  55        apply one_div_pos.mpr
  56        apply sub_pos.mpr
  57        rw [div_lt_one hr]
  58        linarith
  59      · simp [h_rad]
  60        norm_num
  61  }
  62
  63/--- **THEOREM (GROUNDED)**: Existence of static spherical solutions.
  64    For a vacuum region outside a mass M, the Schwarzschild metric provides
  65     a stationary section of the Recognition Science action. -/
  66theorem solution_exists (M : ℝ) :
  67  ∃ (metric : StaticSphericalMetric) (scalar : StaticScalarField),
  68    BoundaryConditions metric := by
  69  use SchwarzschildMetric M, { psi := fun _ => 0 }
  70  unfold BoundaryConditions SchwarzschildMetric
  71  constructor
  72  · -- Limit of 1 - 2M/r as r -> inf is 1
  73    intro ε hε
  74    use 2 * |M| / ε + 1
  75    intro r hr
  76    have : r > 0 := by linarith [abs_nonneg M]
  77    simp
  78    -- |(1 - 2M/r) - 1| = |2M/r| = 2|M|/r < ε
  79    rw [abs_div, abs_of_pos this]
  80    apply div_lt_of_lt_mul
  81    · linarith
  82    · linarith
  83  · -- Limit of 1 / (1 - 2M/r) as r -> inf is 1
  84    intro ε hε
  85    -- Choose R such that 2M/r < 1/2 and (1/(1-x) - 1) < ε
  86    use 4 * |M| * (1 + 1/ε) + 1
  87    intro r hr
  88    have hr_pos : r > 0 := by
  89      have : 4 * |M| * (1 + 1/ε) ≥ 0 := by positivity
  90      linarith
  91    have h_ratio : |2 * M / r| < 1 / 2 := by
  92      rw [abs_div, abs_of_pos hr_pos, div_lt_iff hr_pos]
  93      have : 4 * |M| * (1 + 1/ε) + 1 > 4 * |M| := by
  94        have : 4 * |M| / ε ≥ 0 := by positivity
  95        linarith
  96      have : r > 4 * |M| := by linarith
  97      linarith [abs_of_pos hr_pos]
  98
  99    simp only [sub_add_cancel, abs_sub_comm]
 100    -- |1 / (1 - 2M/r) - 1| = |(2M/r) / (1 - 2M/r)|
 101    have h_denom_pos : 1 - 2 * M / r > 1 / 2 := by
 102      have : 2 * M / r ≤ |2 * M / r| := le_abs_self _
 103      linarith
 104
 105    have h_eq : 1 / (1 - 2 * M / r) - 1 = (2 * M / r) / (1 - 2 * M / r) := by
 106      field_simp [hr_pos.ne', h_denom_pos.ne']
 107
 108    rw [h_eq, abs_div, abs_of_pos h_denom_pos]
 109    apply div_lt_of_lt_mul h_denom_pos
 110    -- We want |2M/r| < ε * (1 - 2M/r)
 111    -- |2M/r| + ε * (2M/r) < ε
 112    -- (2M/r) * (1 + ε) < ε if M > 0
 113    -- |2M/r| * (1 + ε) < ε
 114    -- 2|M|/r * (1 + ε) < ε
 115    -- 2|M|(1 + ε) / ε < r
 116    -- 2|M|(1/ε + 1) < r
 117    have h_r_bound : r > 2 * |M| * (1 / ε + 1) := by
 118      have : 4 * |M| * (1 + 1/ε) + 1 > 2 * |M| * (1 + 1/ε) := by
 119        have : 2 * |M| * (1 + 1/ε) + 1 > 0 := by positivity
 120        linarith
 121      linarith
 122
 123    rw [abs_div, abs_of_pos hr_pos]
 124    have h_goal : 2 * |M| < r * ε * (1 - 2 * M / r) := by
 125      have : r * ε * (1 - 2 * M / r) = ε * r - ε * 2 * M := by ring
 126      rw [this]
 127      -- We need 2|M| < ε*r - 2εM
 128      -- 2|M| + 2εM < ε*r
 129      -- 2|M|(1+ε) < ε*r
 130      -- 2|M|(1+ε)/ε < r
 131      -- 2|M|(1/ε + 1) < r
 132      have h_M_le : 2 * M ≤ 2 * |M| := by linarith [le_abs_self M]
 133      have : ε * 2 * M ≤ ε * 2 * |M| := (mul_le_mul_left hε).mpr h_M_le
 134      have : 2 * |M| * (1 + ε) < ε * r := by
 135        rw [mul_comm ε r, ← div_lt_iff hε]
 136        field_simp [hε.ne']
 137        linarith
 138      linarith
 139    exact h_goal
 140
 141def BoundaryConditions (metric : StaticSphericalMetric) : Prop :=
 142  (∀ ε > 0, ∃ R, ∀ r > R, |metric.f r - 1| < ε) ∧
 143  (∀ ε > 0, ∃ R, ∀ r > R, |metric.g r - 1| < ε)
 144
 145/-!
 146Schwarzschild limit (documentation / TODO).
 147
 148Intended claim: in the appropriate parameter regime, solutions reduce to the Schwarzschild metric.
 149-/
 150
 151end Compact
 152end Relativity
 153end IndisputableMonolith
 154