beta_pot
The beta_pot definition supplies the leading-order post-Newtonian parameter β by returning the constant 1 inside the ILG framework. Researchers comparing ILG to solar-system tests via parametrized post-Newtonian expansions would cite it to recover the GR limit. It is realized as a direct constant assignment that discards its refresh-field and parameter arguments.
claimThe post-Newtonian parameter β is defined by β(ψ, p) := 1 for any refresh field ψ and ILG parameter bundle p.
background
The module supplies potential-based PPN definitions that take a refresh field ψ (an abbreviation for the scalar field appearing in the ILG action) and the global parameter structure p. That structure bundles the coupling constant α together with the lag parameter cLag. The local convention fixes the leading-order values of the PPN coefficients γ and β to their general-relativity values of unity.
proof idea
One-line definition that returns the constant 1.
why it matters in Recognition Science
The definition supplies the GR-matching value of β required by the minimal PPN scaffold in the ILG module. It sits alongside gamma_pot to enforce leading-order equivalence with general relativity before higher-order corrections are introduced. No downstream theorems are recorded yet, marking the entry point for later PPN expansions that will reference the ILG action.
scope and limits
- Does not derive β from the underlying ILG action or field equations.
- Ignores the numerical values of α and cLag stored in ILGParams.
- Supplies no explicit dependence on the refresh field ψ.
- Does not treat post-Newtonian corrections beyond leading order.
formal statement (Lean)
11noncomputable def beta_pot (ψ : RefreshField) (p : ILGParams) : ℝ := 1
proof body
Definition body.
12
13/-- Minimal PPN scaffold: define γ, β to be 1 at leading order (GR limit). -/