SchwarzschildMetric
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
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the metric components from the Recognition Composition Law.
- Does not verify that the metric satisfies the Einstein field equations.
- Does not treat rotating or time-dependent spacetimes.
- Does not compute curvature scalars or geodesic equations.
Lean usage
use SchwarzschildMetric M, { psi := fun _ => 0 }formal statement (Lean)
35noncomputable def SchwarzschildMetric (M : ℝ) : StaticSphericalMetric :=
proof body
Definition body.
36 { f := fun r => if r > 2 * |M| then 1 - 2 * M / r else 1
37 g := fun r => if r > 2 * |M| then 1 / (1 - 2 * M / r) else 1
38 f_positive := by
39 intro r hr
40 by_cases h_rad : r > 2 * |M|
41 · simp [h_rad]
42 -- 1 - 2M/r > 0 ⟺ r > 2M
43 -- We have r > 2|M| and 2|M| ≥ 2M
44 have h_gt : r > 2 * M := by linarith [abs_le_abs_self M, le_abs_self M]
45 apply sub_pos.mpr
46 rw [div_lt_one hr]
47 linarith
48 · simp [h_rad]
49 norm_num
50 g_positive := by
51 intro r hr
52 by_cases h_rad : r > 2 * |M|
53 · simp [h_rad]
54 have h_gt : r > 2 * M := by linarith [abs_le_abs_self M, le_abs_self M]
55 apply one_div_pos.mpr
56 apply sub_pos.mpr
57 rw [div_lt_one hr]
58 linarith
59 · simp [h_rad]
60 norm_num
61 }
62
63/--- **THEOREM (GROUNDED)**: Existence of static spherical solutions.
64 For a vacuum region outside a mass M, the Schwarzschild metric provides
65 a stationary section of the Recognition Science action. -/