solution_exists
plain-language theorem explainer
Existence of static spherical vacuum solutions follows by exhibiting the Schwarzschild metric with vanishing scalar field and verifying the required asymptotic flatness conditions. Workers constructing stationary initial data or rotation curves in Recognition Science cite this result when reducing the action to compact spherical symmetry. The proof is a direct substitution followed by two separate epsilon-delta limit arguments using only field arithmetic and linarith.
Claim. For any real number $M$, there exist positive functions $f,g$ on the positive reals and a real-valued function $psi$ such that both $f(r)$ and $g(r)$ approach 1 as $r$ tends to infinity.
background
StaticSphericalMetric is the structure consisting of two positive real functions $f$ and $g$ defined for $r>0$. StaticScalarField is simply a real function $psi$. BoundaryConditions is the conjunction of two statements requiring that both metric components approach 1 at spatial infinity. The module treats compact static spherical solutions inside the broader Recognition Science treatment of the action, where the Schwarzschild form is asserted to furnish a stationary section outside a central mass.
proof idea
The proof substitutes the explicit SchwarzschildMetric M together with the zero scalar field, then unfolds BoundaryConditions. A constructor splits the conjunction into two independent limits. Each limit is proved by an epsilon-delta argument: choose a sufficiently large R in terms of epsilon and M, then apply abs_div, field_simp, and linarith to bound the deviation below epsilon for all larger r.
why it matters
The result supplies the concrete vacuum solution that downstream theorems invoke when proving existence of rotation velocities (Gravity.RotationILG.solution_exists) and when populating linearized PDE facts (Relativity.NewFixtures.linearizedPDEStub). It directly realizes the doc-comment claim that the Schwarzschild metric supplies a stationary section of the Recognition Science action for vacuum regions outside mass M, thereby anchoring the static spherical case before further extensions to rotation or dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.