f_growth_gr_limit
plain-language theorem explainer
The ILG growth rate in an EdS background equals one when the correction parameter C vanishes. Cosmologists comparing modified gravity to general relativity cite this reduction to recover the standard linear growth result. The proof is a direct simplification that substitutes the zero-C hypothesis into the prefactor definition.
Claim. When the ILG kernel parameter satisfies $C=0$, the growth rate $f(a,k)$ in the EdS background equals 1 for any positive scale factor $a$.
background
The module derives the prefactor for the first-order ILG growth correction in an EdS background by substituting the ansatz $D=a(1+B a^alpha)$ into the growth ODE. KernelParams encodes the model parameters with C as the correction strength. Upstream results include the reciprocity theorem that equates event cost to the cost of its reciprocal and the identity event at the J-cost minimum.
proof idea
This is a one-line wrapper that applies simp to unfold f_growth_eds_ilg and growth_prefactor while substituting the hypothesis that C equals zero.
why it matters
This result shows that the ILG growth factor reduces to the GR value of unity when C vanishes, feeding the parent theorem in ILGGrowthFactor that confirms the same limit. It supplies the consistency check between the ILG model and general relativity inside the Recognition Science framework, aligning with the forcing chain steps that fix D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.