isw_driver_positive
plain-language theorem explainer
The theorem establishes strict positivity of the ISW driver B(a,k) under positive scale factor a, wavenumber k, and kernel parameters with positive alpha and C in the ILG baseline. Cosmologists modeling late-time growth and CMB-LSS cross-correlations would cite it to fix the sign of the Integrated Sachs-Wolfe contribution. The proof unfolds the driver definition, invokes two lemmas establishing f > 1 and dlnw/dlna > 0, then closes with linear arithmetic.
Claim. Let $B(a,k) = -1 + f(a,k) + dlnw/dlna$ denote the ISW driver, where $f$ is the ILG growth rate. For $a > 0$, $k > 0$, and kernel parameters $P$ satisfying $0 < P.alpha$ and $0 < P.C$, it holds that $B(a,k) > 0$.
background
The module formalizes sign logic for the Integrated Sachs-Wolfe driver B(a,k). The driver is defined by unfolding to -1 plus the growth rate f_growth_eds_ilg plus the kernel log-derivative (P.alpha * P.C * Xinv^P.alpha) / (1 + P.C * Xinv^P.alpha) with Xinv = a/(k * P.tau0). KernelParams is the structure bundling the ILG exponent alpha, amplitude C, and reference time tau0. The module doc states that positive B together with negative gravitational potential Phi yields negative CMB-galaxy correlation at low multipoles. Upstream lemmas establish f > 1 (f_growth_gt_one) and dlnw/dlna > 0 (dlnw_pos) under the same positivity hypotheses.
proof idea
The term proof first unfolds isw_driver to expose the expression -1 + f + dlnw. It obtains f > 1 by applying the sibling lemma f_growth_gt_one and dlnw > 0 by applying dlnw_pos. Linarith then combines the two strict inequalities to conclude the sum is positive.
why it matters
This is the main theorem (Target E) of the ISWSign module, closing the positivity claim for the ISW driver in the ILG baseline. It supports the paper statement that positive B with negative Phi produces negative CMB-LSS cross-correlation. In the Recognition framework it confirms growth enhancement consistent with the ILG kernel and phi-derived constants, completing one link in the sign logic for late-time observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.