D_growth
plain-language theorem explainer
The ILG-modified linear growth factor is defined by D(a,k) = a (1 + β(k) a^α)^{1/(1+α)}, where α is the locked fine-structure exponent and β(k) supplies the wavenumber-dependent correction. Cosmologists comparing structure growth under modified gravity to standard GR would cite this closed form when quantifying the enhancement D > a. The definition is a direct algebraic transcription of the formula in the module header.
Claim. The ILG-modified growth factor is given by $D(a,k) = a (1 + β(k) a^α)^{1/(1+α)}$, where $α = (1 - 1/φ)/2$ is the locked exponent and $β(k)$ is the ILG kernel depending on wavenumber $k$ and fundamental tick $τ_0$.
background
The module formalizes growth factors from the dark-energy and Hubble-tension papers. It introduces D(a,k) as the ILG-modified linear growth factor, with the explicit form above, and defines the kernel β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α}. The companion growth rate is f(a,k) = 1 + [α/(1+α)] β a^α / (1 + β a^α). In the GR limit β → 0 one recovers D = a and f = 1 during matter domination; for β > 0 the ILG kernel produces D > a and f > 1.
proof idea
The definition is a direct one-line algebraic expression that composes the sibling beta_growth function with the power-law correction using the locked exponent alphaLock. No tactics or lemmas are applied; the body simply transcribes the formula stated in the module documentation.
why it matters
This definition supplies the central object for the ILG growth analysis. It is invoked by the downstream theorems D_growth_ge_a and D_growth_pos that establish D ≥ a and D > 0, and by the GrowthFactorCert structure that packages the full set of positivity, enhancement, and GR-limit properties. It implements the growth enhancement predicted by the ILG kernel, linking to the phi-based constants and the alphaLock parameter in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.