D_growth_pos
plain-language theorem explainer
The ILG growth factor D(a,k,τ₀) remains strictly positive for every positive scale factor a, wavenumber k, and fundamental tick τ₀. Modelers of structure formation in modified-gravity cosmologies cite the result to guarantee that the growth equations stay well-defined and physically sensible. The proof is a short term-mode reduction that unfolds the explicit formula, applies mul_pos to the leading factor a, invokes beta_growth_pos for the ILG coefficient, and closes with rpow_pos_of_pos plus linarith.
Claim. Let $a>0$, $k>0$, and $τ_0>0$. Then the ILG growth factor $D(a,k,τ_0)>0$, where $D(a,k,τ_0):=a(1+β(k,τ_0)a^α)^{1/(1+α)}$ with $α=α_{lock}=(1-1/φ)/2$ and $β(k,τ_0)=(2/3)φ^{-3/2}(kτ_0)^{-α}$.
background
The module formalizes the ILG-modified linear growth factor and growth rate that appear in the dark-energy and Hubble-tension papers. Its central definition is the noncomputable function D_growth(a,k,τ₀) = a (1 + beta_growth(k,τ₀) a^α)^{1/(1+α)}, where α = alphaLock = (1 − 1/φ)/2 and β(k,τ₀) = (2/3) φ^{-3/2} (k τ₀)^{-α}. The quantity τ₀ is the fundamental tick duration, a positive real constant in RS-native units; alphaLock supplies the locked numerical exponent used throughout the growth expressions.
proof idea
The term-mode proof first unfolds D_growth. It then applies mul_pos to the hypothesis ha : 0 < a. Next it calls Real.rpow_pos_of_pos to obtain 0 < a^α. The key lemma beta_growth_pos (invoked with hk and ht) supplies 0 < β; mul_pos combines this with the positivity of a^α, after which linarith closes the argument on the product inside the power.
why it matters
D_growth_pos supplies the D_positive field of the GrowthFactorCert record, which bundles the core positivity, monotonicity, and GR-limit properties of the ILG growth factor. The result therefore underpins any downstream certification that the modified growth equations remain physically consistent before one invokes the companion statements D_growth_ge_a and D_growth_gr_limit. Within the Recognition framework it closes a basic well-posedness check for the growth sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.