pith. sign in
module module high

IndisputableMonolith.Gravity.BackreactionAudit

show as:
view Lean formalization →

This module audits the Buchert backreaction scalar in ILG gravity. It establishes that Q_D vanishes identically because ILG alters only the source density while preserving the metric and expansion rate, keeping the velocity field irrotational. Researchers in inhomogeneous cosmology would cite these results to confirm zero backreaction within the Recognition Science framework. The module collects targeted lemmas rather than a single central proof.

claimThe Buchert backreaction scalar satisfies $Q_D = 0$ identically for potential-flow velocity fields when the source density is replaced by $w \rho_b$ but the metric and expansion rate remain unmodified.

background

The module sits inside the Recognition Science treatment of gravity and imports the fundamental time quantum $\tau_0 = 1$ tick from IndisputableMonolith.Constants. It centers on the Buchert backreaction scalar $Q_D$, defined as the variance of the expansion rate across a spatial domain $D$. The key premise, stated in the module doc-comment, is that ILG modifies the source term but leaves the metric invariant, so the velocity field stays irrotational and $Q_D$ vanishes.

proof idea

The module structures its argument by recalling that $Q_D = 0$ for any potential-flow velocity field, then invoking the invariance of the metric under ILG source changes. Individual sibling declarations (buchert_Q_D_ilg and related statements) formalize each step; the module level itself contains no single proof body.

why it matters in Recognition Science

This module supports the gravity domain by confirming that ILG introduces no backreaction, consistent with metric preservation in the Recognition Science framework. It has no listed downstream users and therefore stands as an audit result rather than a direct input to a parent theorem.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)