ppn_GR
plain-language theorem explainer
ppn_GR encodes the general-relativistic limit of the parametrized post-Newtonian parameters by setting both γ and β to unity. Workers comparing modified-gravity predictions against solar-system tests would reference this definition to recover the Einstein case. The implementation is a single-line structure literal with no further reduction.
Claim. In general relativity the PPN parameters satisfy $γ = 1$ and $β = 1$.
background
The module treats post-Newtonian potentials in the 1PN approximation. PPNParameters is the structure containing the two real parameters gamma and beta that appear in the metric expansion. Upstream results from ILG.PPN establish that both parameters equal 1 at leading order in the GR limit.
proof idea
The definition is a direct instantiation of the PPNParameters structure with the values gamma := 1 and beta := 1.
why it matters
This definition supplies the GR benchmark against which deviations in the ILG framework are measured. It closes the parameter choice for the metric_1PN components in the post-Newtonian expansion. No open questions are attached at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.