f_growth_gt_one
plain-language theorem explainer
The theorem shows that the ILG growth rate f exceeds 1 whenever the scale factor a, wavenumber k and tick duration tau0 are positive. Cosmologists studying modified gravity or Hubble tension would cite it to confirm faster structure growth than in GR. The proof unfolds the explicit formula for f, invokes positivity of the beta prefactor, and closes via linarith on a chain of strict inequalities built from the locked exponent alphaLock.
Claim. For all positive real numbers $a$, $k$, and fundamental tick duration $τ_0$, the growth rate satisfies $1 < f(a,k,τ_0)$, where $f(a,k) = 1 + [α/(1+α)] ⋅ (β a^α) / (1 + β a^α)$ with locked exponent $α = α_{lock} ≈ 0.191$ and prefactor $β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α}$.
background
The module formalizes the ILG-modified growth factor and rate from the dark-energy and Hubble-tension papers. Core definitions are the growth function $D(a,k) = a (1 + β(k) a^α)^{1/(1+α)}$ and the growth rate $f(a,k) = 1 + [α/(1+α)] β a^α / (1 + β a^α)$, where $α = α_{lock} = (1 - 1/φ)/2$ and $β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α}$. The local setting assumes positive inputs to demonstrate enhancement over the GR limit where $f → 1$ in matter domination. Upstream results supply $α_{lock} > 0$ (alphaLock_pos) and positivity of the beta prefactor (beta_growth_pos).
proof idea
The tactic proof unfolds the definition of f_growth, simplifies, obtains positivity of beta_growth via beta_growth_pos, establishes that $a^α > 0$ and the product term is positive, shows the denominator exceeds 1, verifies the coefficient $α/(1+α) > 0$ using alphaLock_pos, and closes with linarith on the resulting strict inequality.
why it matters
The result is invoked inside growth_factor_cert to certify the full set of ILG growth properties and is reused in the ISWSign module to prove that the ISW driver is strictly positive. It supplies the concrete inequality that distinguishes ILG from the GR limit $f = 1$, supporting the framework's account of enhanced structure formation. No open scaffolding questions are directly closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.