D_growth_gr_limit
plain-language theorem explainer
The theorem establishes that the ILG growth factor reduces exactly to the scale factor a when the modification parameter β vanishes. Cosmologists modeling dark energy or Hubble tension would cite this to confirm recovery of standard GR growth. The proof is a one-line simplification that substitutes β = 0 and applies multiplication and power identities.
Claim. For any $a > 0$, the growth factor in the GR limit satisfies $a · (1 + 0 · a^{α_lock})^{1/(1 + α_lock)} = a$, where $α_lock = (1 - 1/φ)/2$.
background
The module formalizes the ILG-modified growth factor D(a,k) and growth rate f(a,k) from the dark-energy and Hubble-tension papers. Core definitions are D(a,k) = a · (1 + β(k) · a^α)^{1/(1+α)} with β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α} and α = alphaLock ≈ 0.191. The module states that D(a,k) → a as β → 0 (GR limit) and f(a,k) → 1 as β → 0 (matter domination). Upstream alphaLock supplies the locked value α_lock = (1 - 1/φ)/2 as a canonical constant; zero_mul supplies the arithmetic identity zero · n = zero.
proof idea
The proof is a one-line wrapper that applies simp with the lemmas zero_mul and Real.one_rpow to reduce the substituted expression to a after the β = 0 replacement.
why it matters
This result anchors the GR-limit property listed in the module: D(a,k) → a as β → 0. It confirms consistency with standard cosmology in the matter-dominated regime where the growth rate also approaches 1. No downstream theorems are recorded yet, but the declaration closes the recovery claim required by the dark-energy papers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.