StaticScalarField
plain-language theorem explainer
StaticScalarField supplies the scalar component for static spherical configurations in Recognition Science relativity. Workers on vacuum or scalar-extended solutions in the compact sector would cite it when assembling candidate metrics. The declaration is a bare structure definition with no equations or lemmas attached.
Claim. A static scalar field is given by a map $ψ : ℝ → ℝ$.
background
The module Relativity.Compact.StaticSpherical assembles static spherical objects for the Recognition Science action. It imports Geometry.MetricTensor (re-exported as ILG.Action.Metric), Fields.Scalar (whose constant case sets ψ to a fixed real), and the Recognition M structure that supplies the underlying algebra. The vacuum definition from YangMillsMassGap supplies the zero-bond reference case used for the trivial scalar.
proof idea
Structure definition; no lemmas or tactics are invoked.
why it matters
It provides the scalar slot required by the downstream solution_exists theorem, which constructs a vacuum solution by pairing SchwarzschildMetric with the zero scalar field. This places the static spherical sector inside the Recognition Science action and connects it to the vacuum rung-0 configuration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.