localBackreaction
Buchert's local kinematical backreaction is defined by the algebraic expression (2/3)θ² minus 2σ². Cosmologists working on averaged inhomogeneous models cite this when establishing mode-by-mode cancellation under potential flow. The definition consists of a single-line algebraic formula drawn from the standard expression for Q_D.
claim$Q_D(θ, σ²) = (2/3) θ² - 2 σ²$
background
The Buchert averaging formalism introduces the kinematical backreaction Q_D to account for the effects of inhomogeneities on the averaged expansion rate. In this module the local version is isolated for irrotational potential flow, where the variance ⟨θ²⟩ - ⟨θ⟩² collapses to θ². Upstream results supply the shifted cost function H(x) = J(x) + 1, which satisfies H(xy) + H(x/y) = 2 H(x) H(y) and enters the explicit forms of θ and σ² in the cancellation statements.
proof idea
The definition is supplied directly as the algebraic formula (2/3)θ² - 2σ². It serves as a one-line wrapper for the standard Buchert expression and is unfolded in the downstream cancellation proof.
why it matters in Recognition Science
This definition supplies the left-hand side for the buchert_cancellation theorem, which proves that Q_D vanishes for the potential-flow expressions θ = -H f δ and σ² = (1/3) H² f² δ². It thereby establishes the no_background_modification result that the background expansion remains unaltered by averaging. Within Recognition Science this closes the algebraic step linking the functional equation to cosmological homogeneity, consistent with the forced eight-tick octave and three spatial dimensions.
scope and limits
- Does not incorporate vorticity or rotational shear terms.
- Does not perform domain averaging or compute global Q_D.
- Does not depend on the Recognition Science mass ladder or phi scaling.
- Applies strictly in the irrotational limit described in the manuscript.
Lean usage
theorem cancellation_example (H f δ : ℝ) : localBackreaction (-H * f * δ) ((1/3) * (H * f * δ)^2) = 0 := by unfold localBackreaction; ringformal statement (Lean)
24def localBackreaction (θ σ2 : ℝ) : ℝ :=
proof body
Definition body.
25 (2/3 : ℝ) * θ^2 - 2 * σ2
26
27/-- Theorem: For irrotational potential flow, the local backreaction vanishes.
28 From the manuscript:
29 - θ_pec = -H * f * δ
30 - σ^2 = (1/3) * H^2 * f^2 * δ^2
31-/