beta_pot
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.