pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Relativity.Compact.StaticSpherical

show as:
view Lean formalization →

The StaticSpherical module supplies the explicit Schwarzschild metric for vacuum static spherical symmetry with nonzero mass. Compact-object and lensing researchers cite it when modeling horizons or shadow fringes. It is a pure definition module that assembles the metric functions f(r) and g(r) from imported geometry and fields without any 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$ and $g(r) = (1 - 2M/r)^{-1}$ for $r > 2|M|$, extended by a positive constant inside the coordinate singularity.

background

This module aggregates definitions inside the Relativity section of Recognition Science. It imports the Geometry, Calculus, and Fields aggregators to supply the metric components StaticSphericalMetric and SchwarzschildMetric. The setting is vacuum static spherical symmetry (M ≠ 0, ρ = 0, ψ = 0) with the standard spherical line element and the eight-tick octave structure inherited from the parent framework.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the metric used by the Compact module to derive Bekenstein-Hawking entropy from ledger capacity and by Lensing.ShadowPredictions to formalize the 8-tick cycle phase-fringe effect at the event horizon.

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)