Pith. sign in
module module high

IndisputableMonolith.Gravity.BackreactionAudit

show as:
view Lean formalization →

This module audits the Buchert backreaction scalar in ILG gravity and establishes that Q_D vanishes identically. It shows that source modification alone (rho_b to w rho_b) leaves the metric and velocity field unchanged, preserving irrotational potential flow. Researchers in averaged inhomogeneous cosmologies would cite the result to rule out backreaction contributions within the Recognition Science framework. The argument follows from the definition of Q_D together with the ILG source rule.

claimThe Buchert backreaction scalar satisfies $Q_D = 0$ identically when the source is replaced by $w \rho_b$ while the metric and expansion rate are held fixed, so that the velocity field remains irrotational.

background

The Buchert backreaction scalar Q_D measures the variance of the expansion rate across a spatial domain D. For any irrotational (potential-flow) velocity field, Q_D vanishes by definition. ILG, the gravity sector of Recognition Science, replaces the background density source rho_b by w rho_b but leaves the metric tensor and therefore the expansion rate unaltered. The module imports IndisputableMonolith.Constants, whose sole content is the fundamental RS time quantum tau_0 = 1 tick.

proof idea

The module organises a short chain of lemmas (buchert_Q_D_ilg, ilg_preserves_background, X_reciprocity, etc.) that first recall the vanishing of Q_D for potential flow, then verify that ILG source rescaling does not introduce vorticity, and finally conclude Q_D = 0. Each step is a direct algebraic or definitional reduction; no external lemmas beyond the imported Constants are required.

why it matters in Recognition Science

The module supplies the explicit demonstration that backreaction is absent under ILG, thereby closing one consistency check for the Recognition Science gravity sector. It feeds the larger claim that averaged inhomogeneous models reduce to the standard FLRW background when the source is modified in the ILG manner. No downstream theorems are yet recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)