isw_driver
plain-language theorem explainer
This definition supplies the ISW driver B(a,k) as -1 plus the ILG growth rate f plus the weighting term (alpha C Xinv^alpha)/(1 + C Xinv^alpha) with Xinv = a/(k tau0). Cosmologists working on late-time CMB-LSS cross-correlations in modified gravity would cite the expression when deriving the sign of the Integrated Sachs-Wolfe effect. The definition is assembled directly as a term-mode combination of the growth ODE output and the density contrast factor.
Claim. Let $B(a,k) = -1 + f(a,k) + d(a,k)$ where $f(a,k)$ is the growth rate from the ILG ODE and $d(a,k) = (alpha C (a/(k tau_0))^alpha)/(1 + C (a/(k tau_0))^alpha)$ with $tau_0$ the fundamental tick duration.
background
KernelParams holds the ILG model constants alpha (fine-structure constant), C (density weighting), and tau0 (tick duration drawn from RS-native units). The upstream function f_growth_eds_ilg computes the growth factor in the ILG baseline. The module documentation states: 'Because f > 1 and ∂lnw > 0 at late time, the bracket is positive while Phi < 0, yielding a negative CMB–galaxy correlation.'
proof idea
The definition is a direct term-mode computation. It evaluates f via f_growth_eds_ilg, forms Xinv = a/(k P.tau0), assembles the dlnw weighting, and returns the linear combination -1 + f + dlnw.
why it matters
This definition supplies the explicit form of the ISW driver whose positivity is proved in the downstream theorem isw_driver_positive. It implements the bracket in the ILG sign logic for negative CMB-LSS cross-correlation at low multipoles. The construction rests on the growth ODE and the RS constants tau0 and alpha.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.