structure
definition
def or abbrev
StaticScalarField
show as:
view Lean formalization →
formal statement (Lean)
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. -/