localBackreaction
plain-language theorem explainer
The declaration defines the local Buchert backreaction Q_D as (2/3)θ² - 2σ² for mode-by-mode use in averaged cosmologies. Workers on inhomogeneous spacetimes and backreaction cancellation cite it when checking irrotational potential flow. It is supplied as a direct algebraic expression that matches the standard kinematical term.
Claim. $Q_D = (2/3)θ^2 - 2σ^2$, where θ is the expansion scalar and σ² the shear scalar in the irrotational potential flow limit.
background
The module formalizes algebraic cancellation of the Buchert kinematical backreaction Q_D for irrotational potential flow. It states that the ⟨θ²⟩ - ⟨θ⟩² term reduces to θ² in the potential flow limit described in the paper, with references to Dark-Energy.tex showing θ_pec = -H f δ and σ² = (1/3) H² f² δ². Upstream results supply the shifted cost H(x) = J(x) + 1 = ½(x + x^{-1}) that converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
One-line definition that directly encodes the standard Buchert expression Q_D = (2/3)θ² - 2σ².
why it matters
This definition supplies the starting expression for the downstream theorem buchert_cancellation, which proves localBackreaction vanishes under the given θ and σ2, and for no_background_modification, which concludes that the background expansion H(a) remains unaltered by averaging. It fills the module's claim that ILG does not modify H(a) mode-by-mode for potential flow, linking to the Recognition Science cost algebra through the imported H.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.