buchert_Q_D_ilg
plain-language theorem explainer
The definition assigns the value zero to the Buchert backreaction scalar Q_D under the ILG source modification. Cosmologists checking that source weighting leaves the FLRW background intact cite this result. The assignment is a direct constant definition.
Claim. The Buchert backreaction scalar satisfies $Q_D = 0$ in the ILG model.
background
The Buchert backreaction scalar $Q_D$ measures the variance of the expansion rate across a spatial domain $D$. For potential-flow velocity fields this scalar vanishes identically. ILG replaces the source density $rho_b$ by $w rho_b$ while leaving the metric and expansion rate unchanged, so the velocity field remains irrotational and $Q_D$ evaluates to zero. This definition appears in the module that formalizes results from the ILG source-side kernel tests, where zero backreaction is listed among the core results.
proof idea
Direct definition that assigns the real number zero.
why it matters
It supplies the Q_D_zero field required by the BackreactionCert structure, which also encodes X-reciprocity and PPN safety. The definition therefore confirms that late-time anomalies arise from source weighting rather than backreaction, consistent with the framework's separation of source modifications from metric alterations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.