GrowthFactorCert
plain-language theorem explainer
GrowthFactorCert bundles four inequalities asserting that the ILG growth factor D(a,k,τ₀) is positive and at least as large as the scale factor a, that the growth rate f(a,k,τ₀) exceeds 1, and that the kernel parameter β(k,τ₀) is positive, all for positive a, k and τ₀. Cosmologists studying ILG corrections to linear structure formation or Hubble-tension models cite the certificate when they need a compact witness that growth is enhanced relative to the GR baseline. The declaration is a pure structure definition with zero proof body that simply
Claim. The structure GrowthFactorCert asserts that for all $a,k,τ_0>0$ the ILG growth factor satisfies $D(a,k,τ_0)>0$, $D(a,k,τ_0)≥a$ and the growth rate $f(a,k,τ_0)>1$, together with $β(k,τ_0)>0$ for $k,τ_0>0$, where $D(a,k,τ_0)=a(1+β(k,τ_0)a^α)^{1/(1+α)}$, $β(k,τ_0)=(2/3)φ^{-3/2}(kτ_0)^{-α}$ and $f(a,k,τ_0)=1+[α/(1+α)]βa^α/(1+βa^α)$ with $α=α_{Lock}≈0.191$.
background
The module formalizes the ILG-modified linear growth factor and growth rate introduced in the Dark-Energy and Hubble-Tension papers. Core definitions are D(a,k) = a (1 + β(k) a^α)^{1/(1+α)}, β(k) = (2/3) φ^{-3/2} (k τ₀)^{-α} with α = alphaLock ≈ 0.191, and f(a,k) = 1 + [α/(1+α)] β a^α / (1 + β a^α). In the GR limit β → 0 one recovers D = a and f = 1 (matter-dominated growth); for β > 0 both quantities are strictly larger. Upstream results supply the concrete definitions of β_growth, D_growth, f_growth and the fundamental tick τ₀ (appearing in three sibling modules as the RS-native time unit).
proof idea
This is a structure definition with an empty proof body. It aggregates four properties already proved in the sibling lemmas D_growth_pos, D_growth_ge_a, f_growth_gt_one and beta_growth_pos; the downstream theorem growth_factor_cert simply packages those lemmas into an instance of the structure.
why it matters
The certificate is consumed by the theorem growth_factor_cert, which constructs the canonical instance by supplying the four sibling lemmas. It therefore supplies a compact, machine-checked witness that ILG enhances linear growth relative to the GR limit f → 1. The construction sits inside the gravity module that implements the Dark-Energy and Hubble-Tension papers and inherits the RS-native constants (φ, τ₀, alphaLock) already fixed by the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.