BoundaryConditions
plain-language theorem explainer
BoundaryConditions encodes the asymptotic flatness requirement that both metric functions f and g of a static spherical metric tend to 1 at spatial infinity. Researchers constructing static vacuum solutions in Recognition Science cite this predicate to verify that candidate metrics recover the Minkowski limit. The definition is a direct conjunction of two independent limit statements, one for each component.
Claim. Let $(f,g)$ be the components of a static spherical metric. The boundary conditions hold when $f(r)→1$ and $g(r)→1$ as $r→∞$.
background
StaticSphericalMetric packages two positive real-valued functions f and g that serve as the radial coefficients of a static, spherically symmetric line element. The module Relativity.Compact.StaticSpherical develops existence and compactness results for such metrics inside the Recognition Science action. The upstream structure definition supplies the positivity axioms presupposed by the boundary predicate.
proof idea
This is a direct definition that simply conjoins the two epsilon-delta limit statements on f and g. No lemmas or tactics are applied beyond the built-in quantifiers.
why it matters
The predicate is invoked inside solution_exists to certify that the Schwarzschild metric satisfies the required asymptotic behavior, thereby grounding existence of static spherical solutions. It supplies the flat-space boundary datum needed for the static sector of the Recognition Science framework and ensures candidate solutions match the expected Schwarzschild limit at infinity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.