D_growth_ge_a
plain-language theorem explainer
The inequality establishes that the ILG-modified growth factor D(a,k) satisfies D(a,k) >= a for all positive a, k, and tau0. Cosmologists working on modified gravity and Hubble-tension models would cite it to confirm that the ILG kernel never suppresses linear growth below the GR baseline. The proof is a short tactic sequence that unfolds the explicit formula, invokes beta_growth_pos for positivity of the correction term, and closes via Real.one_le_rpow together with linarith.
Claim. Let $a,k,tau_0>0$. Then $a leq D(a,k)$, where the ILG growth factor is $D(a,k)=a(1+beta(k)a^alpha)^{1/(1+alpha)}$ with $alpha=alpha_lock=(1-phi^{-1})/2$ and $beta(k)$ the positive ILG prefactor from beta_growth.
background
The ILGGrowthFactor module encodes the growth factor and growth rate appearing in the Dark-Energy and Hubble-Tension papers. Its central definition is D_growth a k tau0 := a * (1 + beta_growth k tau0 * a ^ alphaLock) ^ (1 / (1 + alphaLock)), which recovers the standard D = a when beta_growth vanishes. alphaLock is the locked fine-structure constant (1 - 1/phi)/2 taken from Constants, while tau0 is the fundamental tick duration re-exported from Compat.Constants and Constants.Derivation. beta_growth supplies the k-dependent ILG kernel that encodes the correction.
proof idea
Unfold D_growth to expose the explicit expression. Obtain 0 < beta_growth k tau0 from beta_growth_pos. Confirm 0 < a ^ alphaLock via Real.rpow_pos_of_pos. Show the inner base 1 + beta * a^alpha >= 1 by linarith. Verify the exponent 1/(1+alphaLock) > 0 using div_pos and alphaLock_pos. Rewrite a as a * 1, apply mul_le_mul_of_nonneg_left, and finish with Real.one_le_rpow.
why it matters
D_growth_ge_a supplies one of the four fields assembled into the GrowthFactorCert record by growth_factor_cert. It therefore underwrites the module claim that D(a,k) > a whenever beta > 0 while recovering equality in the GR limit. In the Recognition Science framework this supplies a concrete quantitative property of the gravity sector that follows from the phi-based forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.