  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.