growth_prefactor
plain-language theorem explainer
The prefactor B(alpha, C) = 3C / (2 alpha^2 + 5 alpha) supplies the linear coefficient in the first-order ILG correction to the growth factor in an EdS background. Cosmologists deriving closed-form growth rates or verifying modified ODEs cite it when working with the ansatz D(a) = a (1 + B (a/(k tau0))^alpha). The definition follows at once from substituting that ansatz into the growth ODE and isolating the O(C) term.
Claim. $B = 3C / (2 alpha^2 + 5 alpha)$ is the prefactor in the first-order ILG growth factor $D(a,k) = a (1 + B (a/(k tau_0))^alpha)$, where alpha is the model exponent and C the coupling strength.
background
In the ILG.GrowthODE module the linear growth factor in an Einstein-de Sitter universe receives a first-order correction controlled by the coupling C. The assumed form is D(a) = a (1 + B X^alpha) with X = a/(k tau0). The upstream alpha definition supplies the fine-structure constant used here as the exponent in the correction term.
proof idea
This is a direct algebraic definition. Substituting the power-law ansatz into the growth ODE and matching the coefficient of the leading correction at linear order in C yields the explicit formula for B.
why it matters
The prefactor is the central building block for growth_eds_ilg and f_growth_eds_ilg. It enables the verification theorem growth_satisfies_ode (ODE compliance to O(C)) and the GR-limit theorem f_growth_gr_limit (recovery of f=1 when C=0). It also supports the X-reciprocity identity and the inequality f>1 in the ILG baseline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.