pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.ILG.GrowthODE

show as:
view Lean formalization →

The GrowthODE module defines the prefactor for the first-order ILG growth correction in an EdS background by substituting the ansatz D = a(1 + B a^alpha) into the growth ODE and incorporating the ILG kernel. Cosmologists studying modified gravity and large-scale structure would cite these definitions when deriving the growth rate f under ILG. The module consists of direct algebraic derivations from the imported kernel and reciprocity objects together with verification lemmas for the resulting ODE.

claimThe module defines the ILG growth prefactor $B$ and the corrected growth function $f$ obtained by substituting the ansatz $D(a) = a(1 + B a^alpha)$ into the EdS growth ODE, using the kernel $w(k,a) = 1 + C (a/(k tau_0))^alpha$ and the dimensionless variable $X = k tau_0 / a$.

background

This module sits inside the ILG formalization and imports the kernel definition w(k,a) = 1 + C · (a / (k τ₀))^α together with the reciprocity variable X = k τ₀ / a. In the Recognition Science setting the ILG kernel modifies the effective gravitational strength at large scales, altering the standard growth equation for the density contrast in an Einstein-de Sitter background. The supplied doc-comment states that the prefactor is obtained by direct substitution of the first-order ansatz D = a(1 + B a^alpha) into that ODE.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the growth prefactor and f_growth_eds_ilg objects that are imported by the ISWSign module. ISWSign uses these to establish the sign of the Integrated Sachs-Wolfe driver, relying on the late-time properties f > 1 and ∂ln w > 0. It thereby fills the growth-correction step required for the ILG prediction of negative CMB-LSS cross-correlation at low multipoles.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)