pith. sign in
module module high

IndisputableMonolith.Relativity.Cosmology.Buchert

show as:
view Lean formalization →

This module defines Buchert's local kinematical backreaction term Q_D for inhomogeneous cosmology models. It states Q_D equals (2/3) theta squared minus 2 sigma squared, with the variance term reducing to theta squared under irrotational potential flow. Researchers examining averaged Einstein equations in relativistic cosmology cite it to assess backreaction effects. The module imports FRWMetric to supply the underlying kinematic scalars and lists sibling declarations that apply the term to cancellation and stability checks.

claimThe Buchert backreaction term is defined by $Q_D = (2/3) theta^2 - 2 sigma^2$, where theta is the expansion scalar and sigma the shear scalar; in the irrotational potential flow limit the averaged variance term reduces to theta squared.

background

The module belongs to the Relativity.Cosmology section and imports the FRWMetric module, which supplies the Friedmann-Robertson-Walker metric together with the kinematic decomposition into expansion, shear, and vorticity. Buchert averaging is the standard procedure that replaces the local Einstein equations by effective equations for the volume-averaged scale factor. The backreaction term Q_D isolates the contribution of local deviations from the mean expansion. The supplied note records that the variance piece ⟨theta squared⟩ minus ⟨theta⟩ squared collapses to theta squared once the flow is restricted to irrotational potential flow.

proof idea

This is a definition module, no proofs. The central content is the direct declaration of the algebraic expression for Q_D together with the one-sentence reduction rule for the irrotational limit.

why it matters in Recognition Science

The definition supplies the central object used by the sibling declarations localBackreaction, buchert_cancellation, no_background_modification, and background_is_stable. It thereby supports the claim that averaged cosmology remains stable without background modification. The module therefore occupies the position of the kinematic starting point for the Recognition Science treatment of Buchert averaging.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)