StaticScalarField
StaticScalarField packages a radial scalar profile psi for static spherical configurations in the Recognition Science relativity module. Researchers constructing stationary solutions of the ILG action cite it when building vacuum sections. The definition is a direct record with a single field psi mapping reals to reals, serving as a placeholder until the coupled ODE system is formalized.
claimA static scalar field is a function $psi : ℝ → ℝ$.
background
The module develops static spherical solutions by combining metric tensors and scalar fields under the ILG action. Upstream, the Scalar module supplies the constant scalar field constructor that sets psi to a fixed real value everywhere. The Recognition structure M and its Cycle3 variant provide the underlying recognition cycle, while the vacuum configuration from the Yang-Mills mass gap sets all gauge bonds to rung zero. The Metric abbrev re-exports the geometry tensor type for use in the action.
proof idea
The declaration is a structure definition that introduces the single field psi. No lemmas or tactics are applied; it is a direct record constructor.
why it matters in Recognition Science
This definition supplies the scalar component required by the solution_exists theorem, which pairs the Schwarzschild metric with a vanishing scalar profile to obtain a stationary vacuum section. It advances the compact-object analysis in the relativity domain and connects to the vacuum state. The field equations remain a documented TODO, marking the next formalization step.
scope and limits
- Does not encode the explicit field equations for psi.
- Does not impose boundary conditions at infinity or the horizon.
- Does not couple psi to the metric components.
- Does not restrict psi beyond the real line.
formal statement (Lean)
20structure StaticScalarField where
21 psi : ℝ → ℝ
22
23-- Field equations would go here (complex ODEs)
24/-!
25Field equations (documentation / TODO).
26
27The static-spherical field equations (coupled ODE/PDE system) are not yet formalized in this module.
28-/
29
30/-- **DEFINITION: Schwarzschild Metric**
31 The static spherical solution for vacuum (M ≠ 0, ρ = 0, ψ = 0).
32 f(r) = 1 - 2M/r, g(r) = (1 - 2M/r)⁻¹ for r > 2|M|.
33 For r ≤ 2|M|, we use a positive constant to satisfy the metric structure
34 outside the coordinate singularity. -/