no_background_modification
plain-language theorem explainer
no_background_modification encodes the algebraic condition that a single Fourier mode with Hubble parameter H, growth rate f and density contrast δ produces zero kinematical backreaction. Cosmologists examining the stability of FLRW backgrounds under inhomogeneities cite this to confirm that potential-flow perturbations leave the expansion history unchanged. The definition is obtained by substituting the mode velocity divergence θ = -H f δ and shear variance σ² = (1/3)(H f δ)² into Buchert's Q_D expression and requiring the result to vanish.
Claim. Let $Q_D(θ,σ²) = (2/3)θ² - 2σ²$. The proposition holds for real numbers $H,f,δ$ precisely when $Q_D(-H f δ, (1/3)(H f δ)²) = 0$.
background
The Buchert equations describe the averaged dynamics of an inhomogeneous universe, with the backreaction term $Q_D$ entering the effective Friedmann equations as a correction to the expansion rate. Here localBackreaction implements the local (mode-by-mode) version $Q_D = (2/3)θ² - 2σ²$, which applies in the irrotational potential-flow limit where variance terms collapse to pointwise values. Upstream, the CostAlgebra.H and FunctionalEquation.H supply the shifted cost function $H(x) = J(x) + 1$ that underlies the Recognition Science functional equation, but in this cosmological context H denotes the background Hubble parameter. The localBackreaction definition records that the peculiar velocity divergence for a growing mode is θ_pec = -H f δ. The module setting is the algebraic cancellation of $Q_D$ for potential flow, even when the growth factor f depends on wavenumber, so that the background expansion H(a) remains that of the chosen matter content.
proof idea
The definition is realized by a direct one-line substitution of the mode parameters into the localBackreaction expression. The body equates localBackreaction(-H f δ, (1/3)(H f δ)²) to zero, which is the explicit statement that the chosen θ and σ² cancel in $Q_D$. No external lemmas are required; the equality follows immediately from the definitions of θ_pec and the shear term supplied in the localBackreaction doc-comment.
why it matters
This supplies the proposition proved by the downstream theorem background_is_stable, which asserts that the background expansion rate is stable under the given mode. It implements the manuscript claim that $Q_D$ cancels mode-by-mode for potential flow, ensuring that the inhomogeneous light-cone geometry does not modify the scale-factor evolution. In the Recognition Science setting the result is consistent with the stability of the homogeneous solution under the forcing chain (T0-T8) and the Recognition Composition Law, with no additional averaging corrections arising from the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.