isw_driver_positive
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish positivity when any of a, k, alpha, or C is non-positive.
- Does not determine the sign of the gravitational potential Phi.
- Does not apply outside the ILG kernel or to alternative growth factors.
- Does not supply numerical bounds or decay rates beyond the strict inequality.
formal statement (Lean)
68theorem isw_driver_positive (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
69 (halpha : 0 < P.alpha) (hC : 0 < P.C) :
70 0 < isw_driver P k a := by
proof body
Term-mode proof.
71 unfold isw_driver
72 have hf := f_growth_gt_one P k a ha hk halpha hC
73 have hd := dlnw_pos P k a ha hk halpha hC
74 linarith
75
76end ILG
77end IndisputableMonolith