ppn_safety_bound
plain-language theorem explainer
This definition certifies that the parametrized post-Newtonian safety condition holds for a characteristic mass of 3e24 and tolerance 1e-5 under the ILG model. Cosmologists testing dark-energy alternatives against precision gravity observations would cite it to confirm recovery of general relativity in the large-X limit. The proof reduces to unfolding the safety predicate and discharging the resulting numerical inequalities by direct normalization.
Claim. The parametrized post-Newtonian safety condition holds for characteristic mass scale $M = 3e24$ and precision tolerance $10^{-5}$.
background
The module formalizes results from the Dark-Energy paper on Buchert backreaction and X-reciprocity. A central claim is PPN safety: in the large-X limit the ILG weight function w tends to 1, recovering general relativity. The definition instantiates this safety check for concrete numerical values drawn from galactic and cluster regimes. Upstream structures supply the ledger factorization and phi-forcing quantities that fix the functional form of w(k,a(z)).
proof idea
One-line wrapper that unfolds the ppn_safe predicate, applies constructor to split the conjunction, and discharges the arithmetic goals with norm_num.
why it matters
It supplies the ppn_ok field inside the BackreactionCert theorem, which assembles zero Buchert backreaction, X-reciprocity from the chain rule, and this PPN safety into a single certificate. The step closes the consistency argument that ILG source modifications remain compatible with solar-system and weak-field tests while permitting the required large-scale adjustments. It directly implements the framework requirement that modifications recover GR when the self-similar parameter X grows large.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.