dlnw_pos
The kernel log-derivative dlnw/dlna is strictly positive in the ILG baseline whenever a > 0, k > 0 and the KernelParams entries alpha, C are positive. Cosmologists modeling the Integrated Sachs-Wolfe effect cite the result to fix the sign of the low-multipole CMB-LSS cross-correlation. The proof substitutes Xinv = a/(k P.tau0), confirms positivity of Xinv and its power via div_pos and rpow_pos_of_pos, then discharges the target by div_pos together with repeated mul_pos and add_pos_of_pos_of_nonneg.
claimFor KernelParams $P$ with $0 < P.α$ and $0 < P.C$, and for real numbers $a > 0$, $k > 0$, the inequality $0 < (P.α · P.C · X^{P.α}) / (1 + P.C · X^{P.α})$ holds, where $X = a / (k · P.τ₀)$ and $τ₀$ is the fundamental tick duration.
background
The ISWSign module formalizes the sign logic for the Integrated Sachs-Wolfe driver B(a,k). A positive driver B combined with negative gravitational potential Phi yields a negative CMB-LSS cross-correlation at low multipoles, as stated in the module reference to Dark-Energy.tex. KernelParams carries the baseline constants alpha (fine-structure constant) and C together with the time unit tau0. Upstream results supply tau0_pos from both Constants and Compat.Constants, each establishing 0 < tau0 by reduction to the positivity of the tick duration; these lemmas are invoked to guarantee that divisions by k · P.tau0 remain positive.
proof idea
The proof sets Xinv := a / (k * P.tau0) and obtains 0 < Xinv by div_pos from ha and mul_pos of hk with tau0_pos. It next shows 0 < Xinv ^ P.alpha via rpow_pos_of_pos. The target inequality is discharged by apply div_pos, with the numerator positive by repeated mul_pos and the denominator positive by add_pos_of_pos_of_nonneg using one_pos together with mul_nonneg on the powered term and C.
why it matters in Recognition Science
The lemma is invoked directly inside isw_driver_positive to conclude that the full ISW driver B(a,k) is strictly positive. It supplies the missing sign for ∂lnw/∂lna required by the ILG baseline argument that f > 1 and ∂lnw > 0 together produce negative CMB-galaxy correlation. The result closes one link in the chain from the kernel definition to observable cross-correlations and is consistent with the framework's derivation of alpha inside the interval (137.030, 137.039).
scope and limits
- Does not compute the numerical magnitude of the derivative.
- Does not apply when a ≤ 0 or k ≤ 0.
- Does not cover non-positive alpha or C.
- Does not incorporate higher-order corrections to the kernel form.
Lean usage
have hd := dlnw_pos P k a ha hk halpha hCformal statement (Lean)
55theorem dlnw_pos (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
56 (halpha : 0 < P.alpha) (hC : 0 < P.C) :
57 0 < (P.alpha * P.C * (a / (k * P.tau0)) ^ P.alpha) / (1 + P.C * (a / (k * P.tau0)) ^ P.alpha) := by
proof body
Term-mode proof.
58 set Xinv := a / (k * P.tau0)
59 have hXinv : 0 < Xinv := div_pos ha (mul_pos hk P.tau0_pos)
60 have hXinv_pow : 0 < Xinv ^ P.alpha := rpow_pos_of_pos hXinv _
61 apply div_pos
62 · repeat apply mul_pos <;> assumption
63 · apply add_pos_of_pos_of_nonneg
64 · exact one_pos
65 · repeat apply mul_nonneg <;> (try exact le_of_lt hC) <;> (try exact le_of_lt hXinv_pow)
66
67/-- Main Theorem (Target E): The ISW driver B(a,k) is strictly positive in ILG baseline. -/