GrowthFactorCert
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
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit functional forms of D_growth or beta_growth.
- Does not fix the numerical value of alphaLock or its origin.
- Does not address nonlinear regimes or higher-order perturbations.
- Does not incorporate observational constraints on the Hubble tension.
formal statement (Lean)
130structure GrowthFactorCert where
131 D_positive : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → 0 < D_growth a k tau0
132 D_ge_a : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → a ≤ D_growth a k tau0
133 f_gt_one : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → 1 < f_growth a k tau0
134 beta_positive : ∀ k tau0 : ℝ, 0 < k → 0 < tau0 → 0 < beta_growth k tau0
135