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

IndisputableMonolith.ILG.ISWSign

show as:
view Lean formalization →

The ILG.ISWSign module defines the ISW driver B(a,k) = -1 + f + dlnw/dlna for the Infra-Luminous Gravity framework. It assembles the driver from the kernel w(k,a) and the growth prefactor B supplied by GrowthODE. Cosmologists modeling modified gravity corrections to large-scale structure and the integrated Sachs-Wolfe effect would cite this module. The module consists of direct definitions and positivity lemmas built on the two imported modules.

claim$B(a,k) = -1 + f + dlnw/dln a$, where $w(k,a) = 1 + C (a/(k τ_0))^α$ is the ILG kernel and $f$ is the growth rate obtained from the first-order correction $D = a(1 + B a^α)$ in an EdS background.

background

The ILG kernel module supplies the scale-dependent weight $w(k,a) = 1 + C (a/(k τ_0))^α$ that modifies gravitational clustering at infra-luminous scales. The GrowthODE module derives the prefactor B by substituting the ansatz $D = a(1 + B a^α)$ into the linear growth equation for an EdS background. The present module combines these objects to form the ISW driver, which enters the time derivative of the gravitational potential relevant for CMB temperature anisotropies.

proof idea

This is a definition module, no proofs. It introduces the ISW driver together with auxiliary statements (isw_driver, f_growth_gt_one, dlnw_pos, isw_driver_positive) by direct substitution of the kernel and growth prefactor imported from Kernel and GrowthODE.

why it matters in Recognition Science

The module supplies the ISW driver required for computing the integrated Sachs-Wolfe signal in ILG cosmology. It closes the chain from the kernel definition through the growth correction to an observable large-scale structure signature. No downstream theorems are listed, indicating the driver is intended as an interface for subsequent ILG calculations of CMB and matter power spectra.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)