f_growth_gt_one
plain-language theorem explainer
In the ILG baseline the growth rate exceeds unity for positive scale factor, wavenumber and kernel parameters. Cosmologists working on late-time structure formation or ISW effects would cite this to establish that the growth factor is super-linear. The proof proceeds by introducing the auxiliary quantity Xinv = a/(k tau0), verifying positivity of the prefactor B and the powered term, then reducing the inequality via field simplification and positivity of the added term.
Claim. Let $P$ be kernel parameters with $0 < P.alpha$ and $0 < P.C$. For $a > 0$ and $k > 0$, the ILG effective dark sector growth rate satisfies $1 < f_{growth,eds,ilg}(P,k,a)$.
background
The module formalizes sign logic for the Integrated Sachs-Wolfe driver B(a,k). KernelParams supplies the ILG model parameters alpha and C. The function f_growth_eds_ilg is the growth rate (1 + B(1+alpha)X^alpha)/(1 + B X^alpha) with X = a/(k tau0) and B the growth prefactor drawn from GrowthODE. Upstream results supply tau0 as the fundamental tick duration together with the lemma tau0_pos establishing 0 < tau0, and alpha as the fine-structure constant.
proof idea
The proof sets Xinv := a / (k * P.tau0) and B := growth_prefactor P.alpha P.C. It establishes 0 < B by unfolding the definition and applying div_pos. Positivity of Xinv follows from div_pos using ha, hk and tau0_pos. It then unfolds f_growth_eds_ilg, applies field_simp, and uses lt_add_of_pos_right together with div_pos on the remainder term, verifying the numerator and denominator are positive via repeated mul_pos and add_pos_of_pos_of_nonneg.
why it matters
This result feeds the main theorem isw_driver_positive which shows the ISW driver is strictly positive. It also appears in growth_factor_cert which certifies D positive, D ge a, f gt one and beta positive. In the Recognition framework it supports the claim that ILG enhances the growth rate beyond the Einstein-de Sitter value of unity, consistent with the late-time behavior required for a negative CMB-galaxy correlation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.