solution_exists

formal source

  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