ppn_safe
plain-language theorem explainer
ppn_safe encodes the parameter constraints on X_safe and epsilon that guarantee the ILG weight function stays within epsilon of unity for X at or above X_safe. Gravitational physicists testing modified gravity against solar-system data would reference this predicate when confirming consistency with post-Newtonian bounds. The definition consists of a direct conjunction of three strict inequalities on the real numbers.
Claim. The predicate ppn_safe($X_{safe}$, $epsilon$) holds precisely when $X_{safe} > 0$, $epsilon > 0$, and $epsilon < 1$. These bounds ensure that the ILG weight function $w(X)$ satisfies $|w(X) - 1| ≤ epsilon$ for all $X ≥ X_{safe}$.
background
The module formalizes results from the Dark-Energy paper on Buchert backreaction and X-reciprocity. ILG modifies sources via a weight function $w(X)$ that approaches 1 for large $X$, recovering general relativity in the solar system where $X >> 10^{30}$. The predicate supplies the formal regime in which the deviation remains bounded by epsilon. Upstream, Energy is an abbreviation for the reals, and the from theorem extracts four structural conditions plus three definitional facts from seven independent axioms.
proof idea
The definition is a direct conjunction of the three inequalities $0 < X_{safe}$, $0 < epsilon$, and $epsilon < 1$. No lemmas or tactics are invoked; the body is the predicate itself.
why it matters
This definition is instantiated inside BackreactionCert as the ppn_ok field with the paper values $X_{safe} = 3e24$ and $epsilon = 1e-5$. It certifies that ILG recovers GR at solar-system scales while preserving zero Buchert backreaction and X-reciprocity. The construction supports the E_G factorization and monotonicity results that follow in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.