StaticSphericalMetric
StaticSphericalMetric defines the data for a static spherically symmetric metric via two positive functions f(r) and g(r) on r > 0. Researchers constructing exact solutions in Recognition Science relativity cite it as the basic type for stationary vacuum metrics. The definition is a pure structure whose only content is the positivity axioms on the radial functions.
claimA static spherical metric consists of functions $f, g : (0,∞) → ℝ$ such that $f(r) > 0$ and $g(r) > 0$ for every $r > 0$.
background
The structure lives in the Relativity.Compact.StaticSpherical module, which develops compact static solutions under the Recognition Science action. It imports basic real analysis and geometry from sibling modules but depends on no prior theorems. Positivity of f and g guarantees a valid Lorentzian signature in the spatial sector for r > 0, consistent with the D = 3 spatial dimensions of the framework.
proof idea
This is a pure structure definition. It introduces the two function fields together with their positivity conditions as part of the type; no tactics or lemmas are applied.
why it matters in Recognition Science
StaticSphericalMetric supplies the parent type for BoundaryConditions (asymptotic flatness) and for the concrete SchwarzschildMetric construction. These in turn feed the theorem solution_exists, which asserts existence of vacuum static spherical solutions. The structure therefore supplies the metric ansatz required by the Recognition Science forcing chain once the eight-tick octave and spatial dimension D = 3 are fixed.
scope and limits
- Does not impose any differential equations or field equations on f or g.
- Does not incorporate time dependence or non-spherical perturbations.
- Does not include the scalar field or matter content.
- Does not address coordinate singularities, horizons, or interior matching.
formal statement (Lean)
14structure StaticSphericalMetric where
15 f : ℝ → ℝ
16 g : ℝ → ℝ
17 f_positive : ∀ r, r > 0 → f r > 0
18 g_positive : ∀ r, r > 0 → g r > 0
19