beta_def
plain-language theorem explainer
beta_def delivers a named alias for the PPN β coefficient fixed at unity, enabling clean citations in papers on parametrized post-Newtonian gravity. Researchers testing the ILG model against solar-system data would reference it to confirm the standard GR value. The declaration is implemented as a one-line abbreviation of the beta definition from the same module.
Claim. The PPN parameter $β$ is defined by $β(C_{lag}, α) := 1$, independent of the lag and coupling parameters.
background
The module supplies potential-based PPN definitions as a scaffold that expresses post-Newtonian parameters through the gravitational potentials Φ and Ψ derived from ψ and model parameters. The upstream beta definition in the same module states that the PPN β coefficient equals 1 for any real inputs C_lag and α. Related upstream results include the System structure, defined as a collection of energy levels with nonempty list, and the thermodynamic beta as the inverse temperature 1/(k_B T).
proof idea
This is a one-line wrapper that directly applies the beta definition from the PPN module.
why it matters
This definition supplies the reference value for the PPN β parameter in the ILG framework, matching the general relativity prediction of unity. It supports the beta_bound and beta_lin siblings that state solar-system style bounds such as |β−1| ≤ 1/100000. The module doc-comment positions the entry as part of the potential-based PPN scaffold for paper reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.