ppn_safe
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not define the explicit functional form of the weight function w(X).
- Does not prove that w approaches 1 as X grows.
- Does not supply the numerical value of X_safe from observations.
- Does not address dependence on scale factor or wavenumber.
Lean usage
def ppn_safety_bound : ppn_safe 3e24 (1e-5) := by unfold ppn_safe; constructor <;> norm_numformal statement (Lean)
77def ppn_safe (X_safe epsilon : ℝ) : Prop :=
proof body
Definition body.
78 0 < X_safe ∧ 0 < epsilon ∧ epsilon < 1
79
80/-- The PPN safety parameters from the Dark-Energy paper. -/