pith. sign in
module module high

IndisputableMonolith.Relativity.Compact.StaticSpherical

show as:
view Lean formalization →

The StaticSpherical module defines the Schwarzschild metric as the static spherical vacuum solution in the Recognition Science relativity framework. It specifies the metric functions f(r) and g(r) for M nonzero and vanishing density and scalar field. Researchers on compact objects and black hole lensing cite it. The module aggregates imported geometry, calculus, and fields definitions with no internal proofs.

claimThe Schwarzschild metric is the vacuum static spherical solution $ds^2 = -f(r) dt^2 + g(r) dr^2 + r^2 d\Omega^2$ where $f(r) = 1 - 2M/r$, $g(r) = (1 - 2M/r)^{-1}$ for $r > 2|M|$, and a positive constant replaces the expression for $r \leq 2|M|$.

background

This module resides in the Relativity domain and re-exports components from the Geometry, Calculus, and Fields aggregator modules. Its central object is the SchwarzschildMetric for vacuum cases (M ≠ 0, ρ = 0, ψ = 0). The supplied doc-comment states: "The static spherical solution for vacuum (M ≠ 0, ρ = 0, ψ = 0). f(r) = 1 - 2M/r, g(r) = (1 - 2M/r)⁻¹ for r > 2|M|. For r ≤ 2|M|, we use a positive constant to satisfy the metric structure outside the coordinate singularity."

Sibling declarations introduce StaticSphericalMetric, StaticScalarField, solution_exists, and BoundaryConditions. These support the ds² = -f(r)dt² + g(r)dr² + r²dΩ² form used in downstream compact-object work.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the vacuum metric definition to the parent Compact module, which builds static spherically symmetric solutions and BlackHoleEntropy from ledger capacity. It also feeds Lensing.ShadowPredictions, whose objective is to prove that the 8-tick cycle creates a detectable phase fringe at the event horizon. It therefore anchors the T7 eight-tick octave structure inside the static spherical sector.

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)