Gravity Backreaction Audit

The backreaction audit

In cosmology, backreaction is the effect of small-scale structure on the large-scale expansion of the universe. The Buchert backreaction scalar Q_D measures the variance of the expansion rate across a spatial domain D. When Q_D is zero, the background expansion behaves exactly as in the standard homogeneous model, and no late-time acceleration is explained by backreaction. The question is whether a proposed modification of gravity, called ILG, accidentally introduces such backreaction.

The audit establishes that it does not. ILG modifies the source term in Einstein's equations, replacing the matter density rho_b with w * rho_b, where w is a scale-dependent weight function. It does not modify the metric or the expansion rate itself. Because the velocity field remains irrotational, a potential flow, the backreaction scalar vanishes identically. The theorem buchert_backreaction_zero states this directly: buchert_Q_D_ilg = 0. A second theorem, ilg_preserves_background, extends this to all scale factors a, confirming that ILG does not alter the background FLRW evolution at any time.

The audit then checks three further properties. First, X-reciprocity: for any observable that depends only on the dimensionless variable X = k * tau0 / a, the logarithmic derivative with respect to scale a equals minus the derivative with respect to wavenumber k. This follows from the chain rule, since ln X = ln k + ln tau0 - ln a. Second, PPN safety: in the large-X limit, the weight function w approaches 1, recovering general relativity. The audit fixes X_safe = 3e24 for epsilon_PPN = 1e-5, meaning that for X above this threshold, the deviation from GR is below one part in 100,000. In the solar system, X is far larger than 10^30, so ILG is observationally indistinguishable from GR there. Third, the E_G statistic, which measures gravitational lensing versus growth, factorizes as (Omega_s0 / f) * w, a product of two computable functions, and is positive when all inputs are positive.

All of these results are packaged into a single certificate, BackreactionCert, which bundles the three key properties: zero backreaction, X-reciprocity, and PPN safety. The certificate is a theorem in the framework's machine-checked library of formal theorems. In plain language, the audit says: this modification changes how matter sources gravity, but it does not change how the universe expands, and it reduces to ordinary gravity in the solar system. The late-time anomalies that ILG addresses must therefore come from source weighting, not from backreaction.

theorem buchert_backreaction_zero : buchert_Q_D_ilg = 0 := rfl

/-- Q_D = 0 means ILG does not alter the background FLRW evolution.
    Late-time anomalies arise from SOURCE weighting, not backreaction. -/
theorem ilg_preserves_background :
    buchert_Q_D_ilg = 0 ∧ (∀ a : ℝ, 0 < a → buchert_Q_D_ilg = 0) :=
  ⟨rfl, fun _ _ => rfl⟩

/-- The PPN safety parameters from the Dark-Energy paper. -/
def ppn_safety_bound : ppn_safe 3e24 1e-5 := by
  unfold ppn_safe; constructor <;> norm_num

theorem backreaction_cert : BackreactionCert where
  Q_D_zero := buchert_backreaction_zero
  reciprocity := X_reciprocity_from_chain_rule
  ppn_ok := ppn_safety_bound

What this page does not claim

The audit does not prove that ILG is the correct theory of gravity. The audit does not derive the weight function w(X) from first principles. The audit does not show that backreaction is absent in all modified gravity theories.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/BackreactionAudit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: