ppn_safe
plain-language theorem explainer
The predicate on the safe scale and tolerance parameters encodes the conditions needed to guarantee that the ILG weight function recovers general relativity at large X. Cosmologists testing modified gravity would cite this when verifying solar-system PPN compliance. It consists of the direct conjunction of three inequalities on the real parameters.
Claim. The predicate holds precisely when the safe scale parameter is positive, the tolerance parameter is positive, and the tolerance is strictly less than one. This encodes the requirement from the Dark-Energy paper that the ILG weight function satisfies a deviation bound of epsilon for all scales at or above the safe scale.
background
The BackreactionAudit module formalizes key results from the Dark-Energy paper on ILG: zero Buchert backreaction, X-reciprocity between scale and time slopes, PPN safety where the weight function approaches 1 at large X to recover GR, and E_G factorization. PPN safety is formalized via this predicate on the parameters. The paper states the safe scale approximately 3 times 10 to the 24 for tolerance equal to 10 to the minus 5, with solar-system values much larger. Upstream, Energy is defined as the real numbers and the from theorem derives four structural conditions plus three definitional facts from seven axioms.
proof idea
This definition directly states the conjunction of the three inequalities on the input parameters. The downstream safety bound applies unfold followed by norm_num to discharge the concrete instance with values 3e24 and 1e-5.
why it matters
This predicate supplies the condition asserted as safety inside the BackreactionCert structure, which also encodes zero Buchert backreaction and X-reciprocity. It implements the PPN safety claim from the Dark-Energy paper, ensuring the weight function is within epsilon of unity for scales at or above the safe scale. The result supports the gravity domain by closing the safety check in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.