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 shows that the scalar vanishes because source rescaling alone leaves the velocity field irrotational. Researchers in inhomogeneous cosmology cite it to drop backreaction terms. The argument rests on the metric and expansion rate remaining unchanged under the ILG modification.

claimThe Buchert scalar $Q_D$ satisfies $Q_D = 0$ for any potential-flow velocity field when the source is replaced by $w$ times the background density while the metric and expansion rate stay fixed.

background

The Buchert backreaction scalar $Q_D$ measures the variance of the expansion rate across a spatial domain $D$. It vanishes for irrotational velocity fields by a standard identity in inhomogeneous cosmology. The ILG construction modifies only the source term from background density to a weighted version but leaves the metric and expansion rate untouched, so the velocity field remains a gradient field.

proof idea

The module structures its argument as a sequence of targeted lemmas on reciprocity, positivity, and monotonicity. These establish that the source change introduces no vorticity. The zero result for the backreaction scalar then follows directly from the potential-flow identity.

why it matters in Recognition Science

This module certifies the absence of backreaction in the ILG setting and feeds the main gravity consistency theorems. It closes the audit step that justifies homogeneous background evolution within the Recognition Science framework. The result aligns with preservation of the underlying potential flow under the eight-tick structure.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)