StaticScalarField
plain-language theorem explainer
StaticScalarField defines the type of a static scalar field on the radial line as a map from reals to reals. Researchers constructing explicit vacuum solutions in the Recognition Science treatment of static spherical symmetry cite it when supplying the scalar component. The declaration is a bare structure definition with no attached equations or computational content.
Claim. A static scalar field is a function $ψ : ℝ → ℝ$.
background
The Relativity.Compact.StaticSpherical module assembles types for static spherical metrics and fields inside the Recognition Science action. Upstream, Relativity.Fields.Scalar.constant supplies the constant scalar field {ψ := fun _ => c}. Recognition.M and Cycle3.M provide the underlying recognition structure M that enters the action functional. Relativity.ILG.Action.Metric re-exports the metric tensor type, while YangMillsMassGap.vacuum records the zero-bond configuration at rung zero.
proof idea
This declaration is a direct structure definition with no proof body.
why it matters
It supplies the scalar field argument to solution_exists, which constructs the Schwarzschild metric paired with the zero scalar field and verifies the boundary conditions. That theorem asserts the Schwarzschild solution forms a stationary section of the Recognition Science action in the vacuum region. The construction sits inside the compact static setting that inherits the eight-tick octave and D = 3 from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.