buchert_cancellation
plain-language theorem explainer
For irrotational potential flow the local Buchert backreaction vanishes identically when the divergence satisfies θ = -H f δ and the shear variance satisfies σ² = (1/3)(H f δ)². Cosmologists working on averaged inhomogeneous models in the Recognition Science setting cite the result to confirm that the background expansion rate H(a) is left unmodified by averaging. The proof is a short algebraic reduction that unfolds the backreaction definition and normalizes the resulting polynomial identity.
Claim. Let $H, f, δ ∈ ℝ$. Define $θ := -H f δ$ and $σ² := (1/3)(H f δ)²$. Then the local kinematical backreaction term vanishes: $Q(θ, σ²) = 0$.
background
The Buchert formalism averages the Einstein equations over finite spatial domains and introduces a kinematical backreaction term Q_D that modifies the effective Friedmann equations. This module isolates the local contribution to Q_D and shows exact cancellation for irrotational potential flow. The module doc-comment states: “The Buchert kinematical backreaction Q_D cancels mode–by–mode for potential flow even when f depends on k; thus ILG does not alter H(a) by averaging.”
proof idea
The tactic proof begins with dsimp to expose the let-bindings, unfolds the localBackreaction definition, clears denominators via field_simp, and closes the resulting polynomial identity with the ring tactic over the reals.
why it matters
The theorem is applied directly by background_is_stable to conclude no_background_modification, establishing that the background Hubble rate remains that of the chosen matter content. It implements the manuscript claim that Q_D cancels for potential flow, preserving the Friedmann-Lemaître expansion history inside the Recognition Science framework. It touches the open question whether global domain averaging could still generate an effective dark-energy term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.