background_is_stable
plain-language theorem explainer
The theorem establishes that the background Hubble rate H(a) experiences no modification from Buchert averaging when the flow is irrotational and potential. Cosmologists studying backreaction in inhomogeneous models would cite it to retain the standard FLRW expansion history. The proof is a one-line term application of the prior cancellation result for the local backreaction term.
Claim. For real numbers $H$, $f$, and $δ$, the local backreaction vanishes: localBackreaction$(-H f δ, (1/3)(H f δ)^2) = 0$.
background
In the Buchert formalism the kinematical backreaction $Q_D$ is built from the peculiar expansion deviation $θ$ and the shear scalar $σ^2$. The module defines localBackreaction $θ σ^2$ as the combination that produces $Q_D$ after volume averaging. The upstream result buchert_cancellation supplies the explicit relations $θ = -H f δ$ and $σ^2 = (1/3) H^2 f^2 δ^2$ that hold for irrotational potential flow. The companion definition no_background_modification simply asserts that this combination equals zero, so the averaged expansion rate remains that of the chosen background matter content.
proof idea
The proof is a direct term-mode application of the buchert_cancellation theorem, which itself unfolds localBackreaction and performs the algebraic cancellation of the two quadratic terms.
why it matters
The declaration closes the no_background_modification property inside the Buchert module, confirming that the background expansion history is stable under averaging for potential flow. It directly implements the manuscript claim that $Q_D$ cancels mode-by-mode even when the growth factor $f$ depends on wavenumber, thereby preserving the standard FLRW background in the Recognition Science treatment of cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.