SchwarzschildMetric
plain-language theorem explainer
The SchwarzschildMetric definition supplies the explicit radial functions f and g for the static spherical vacuum solution, with a piecewise constant extension inside the coordinate horizon to keep both components positive. Researchers constructing stationary sections of the Recognition Science action for compact objects would cite this when instantiating the StaticSphericalMetric structure. The definition proceeds by direct term construction of the two functions followed by case analysis on the radial threshold to discharge the positivity side
Claim. The Schwarzschild metric is the pair of functions $(f,g)$ on the positive reals where $f(r)=1-2M/r$ and $g(r)=(1-2M/r)^{-1}$ whenever $r>2|M|$, while both equal the constant 1 otherwise, satisfying the positivity axioms $f(r)>0$ and $g(r)>0$ for all $r>0$.
background
StaticSphericalMetric is the structure requiring two functions $f,g:ℝ→ℝ$ together with proofs that both remain strictly positive for every positive radius. The module places this definition inside the compact static spherical sector of the Recognition Science relativity development, where vacuum regions outside a central mass are represented by stationary sections of the action. Upstream dependencies supply the J-cost convexity and ledger factorization structures that underwrite the broader action principle, though the present definition itself rests only on elementary real arithmetic.
proof idea
The definition is a direct term-mode construction of the record {f,g,f_positive,g_positive}. Each positivity field performs a by_cases split on whether r exceeds 2|M|, then applies linarith together with sub_pos and one_div_pos to obtain the required strict inequalities in the exterior region while the interior case collapses to norm_num.
why it matters
This definition supplies the concrete metric that the downstream solution_exists theorem instantiates to witness existence of static spherical vacuum solutions. It thereby fills the explicit-construction step in the Recognition Science treatment of stationary compact objects, linking the general StaticSphericalMetric interface to the vacuum case outside a mass M. The construction respects the framework requirement that metric components remain positive, consistent with the eight-tick local dynamics and J-cost minimization already established in the foundation modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.