growth_factor_cert
plain-language theorem explainer
Growth factor certificate asserts that the ILG density contrast D remains positive and at least as large as the scale factor a for positive inputs, while the growth rate f exceeds one and the prefactor β stays positive. Cosmologists modeling dark energy or Hubble tension via ILG modifications cite it to confirm the growth equations obey the required inequalities. The proof is a direct term construction that assembles the four component lemmas into the GrowthFactorCert structure.
Claim. For all real $a, k, τ_0 > 0$, the ILG density contrast satisfies $D(a,k,τ_0) > 0$ and $D(a,k,τ_0) ≥ a$, the growth rate satisfies $f(a,k,τ_0) > 1$, and the prefactor satisfies $β(k,τ_0) > 0$, where $D(a,k,τ_0) = a (1 + β(k,τ_0) a^α)^{1/(1+α)}$ with $β(k,τ_0) = (2/3) φ^{-3/2} (k τ_0)^{-α}$ and $f$ the corresponding growth rate, $α = α_{Lock}$.
background
The ILG Growth Factor module encodes the modified growth equations from the dark-energy and Hubble-tension papers. Core definitions are $D(a,k) = a (1 + β a^α)^{1/(1+α)}$ and $f(a,k) = 1 + [α/(1+α)] β a^α / (1 + β a^α)$, with $β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α}$ and $α ≈ 0.191$. These recover the GR limits $D = a$ and $f = 1$ when β vanishes.
proof idea
Term proof that constructs the GrowthFactorCert instance by field assignment. It maps D_positive to D_growth_pos, D_ge_a to D_growth_ge_a, f_gt_one to f_growth_gt_one, and beta_positive to beta_growth_pos. The construction relies on the structure definition and the four component theorems.
why it matters
Supplies a single certified object for the ILG growth properties used in dark-energy modeling. It aggregates the module's positivity lemmas, enabling direct reference in cosmological calculations. Within Recognition Science this supports consistency checks for the ILG extension, though it does not invoke the forcing chain T0-T8 or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.