pith. sign in
module module high

IndisputableMonolith.Relativity.Compact.StaticSpherical

show as:
view Lean formalization →

This module defines the Schwarzschild metric as the static spherical vacuum solution with f(r) = 1 - 2M/r and g(r) = (1 - 2M/r)^{-1} for r > 2|M|. Researchers working on compact objects or black hole lensing would cite it when importing the metric into entropy or shadow calculations. It is a definition module that aggregates geometry, calculus, and fields without internal proofs.

claimThe Schwarzschild metric takes the form $ds^2 = -f(r)dt^2 + g(r)dr^2 + r^2 dΩ^2$ with $f(r) = 1 - 2M/r$, $g(r) = (1 - 2M/r)^{-1}$ for $r > 2|M|$, and a positive constant inside the coordinate singularity; this is the unique static spherical vacuum solution ($M ≠ 0$, $ρ = 0$, $ψ = 0$).

background

The module lives in the Relativity domain and re-exports components from Geometry, Calculus, and Fields. Its central object is the static spherically symmetric line element $ds^2 = -f(r)dt^2 + g(r)dr^2 + r^2 dΩ^2$ together with the explicit Schwarzschild functions. Sibling definitions include StaticSphericalMetric, StaticScalarField, solution_exists, and BoundaryConditions. The setting matches the downstream description of static spherically symmetric solutions used for entropy and lensing.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies SchwarzschildMetric to the parent Compact module (which derives BlackHoleEntropy from ledger capacity) and to Lensing.ShadowPredictions (which formalizes ILG-corrected shadow fringes at the event horizon). It therefore supplies the concrete vacuum solution required for any downstream claim that the eight-tick cycle produces observable phase structure around static compact objects.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)