f_growth_gr_limit
plain-language theorem explainer
f_growth_gr_limit shows that the ILG growth rate equals 1 at a=1, k=1, tau0=0, recovering the GR limit. Cosmologists modeling structure formation with ILG corrections cite it for consistency with standard cosmology. The proof is a direct unfolding of f_growth and beta_growth followed by arithmetic simplification via zero-product lemmas.
Claim. The ILG-modified growth rate satisfies $f(1,1,0)=1$, where $f(a,k)$ is defined by $f=1 + [α/(1+α)] β a^α / (1 + β a^α)$ and β(k,τ₀)=(2/3)φ^{-3/2}(k τ₀)^{-α} with α=alphaLock.
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+α)}, β(k)=(2/3)φ^{-3/2}(k τ₀)^{-α}, and f(a,k)=1+[α/(1+α)] β a^α/(1+β a^α), with α=alphaLock≈0.191. The GR limit is the case β→0, which yields f→1 in matter domination.
proof idea
The proof unfolds the definitions of f_growth and beta_growth. The simp tactic then applies mul_zero, Real.rpow_zero, and zero_mul to reduce the resulting expression directly to 1.
why it matters
This confirms the GR limit property f→1 as β→0 for the growth rate, feeding the parent theorem f_growth_gr_limit in IndisputableMonolith.ILG.GrowthODE. It matches the module key property that f(a,k)→1 as β→0 and supports consistency with standard results in the Recognition Science gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.