f_growth
plain-language theorem explainer
The ILG growth rate is defined as the logarithmic derivative of the growth factor D under the modified-gravity kernel. Cosmologists modeling structure formation or Hubble tension would cite the expression when evaluating enhanced clustering relative to general relativity. The definition is a direct algebraic assembly that substitutes the growth kernel into a weighted fraction involving the locked exponent.
Claim. $f(a,k)=1+frac{alpha}{1+alpha}frac{beta a^alpha}{1+beta a^alpha}$, where $alpha=(1-1/phi)/2approx0.191$, $beta(k,tau_0)=(2/3)phi^{-3/2}(k tau_0)^{-alpha}$, and $tau_0$ is the fundamental tick duration.
background
The module encodes the ILG growth factor and rate drawn from the dark-energy and Hubble-tension papers. The growth factor itself reads $D(a,k)=a(1+beta(k)a^alpha)^{1/(1+alpha)}$ with kernel $beta(k)=(2/3)phi^{-3/2}(k tau_0)^{-alpha}$ and locked exponent $alpha=alphaLock=(1-1/phi)/2$. The rate $f$ is obtained as $dlnD/dln a$, which expands algebraically to the displayed form. In the general-relativity limit $beta=0$ one recovers $f=1$ during matter domination. Upstream, the kernel is supplied by beta_growth, the exponent by alphaLock (derived from the golden-ratio relation), and the time scale by tau0 from the constants derivation.
proof idea
The definition binds beta to the result of beta_growth, forms the auxiliary product beta times a to the power alphaLock, and assembles the weighted fraction (alphaLock over 1 plus alphaLock) times that product over one plus the product. It is a direct let-binding expression requiring no lemmas or tactics beyond the kernel definition.
why it matters
This supplies the growth-rate factor that enters the E_G statistic in the backreaction audit and the growth-factor certificate structure. It encodes the ILG enhancement formula from the referenced papers, recovering the general-relativity value of unity when the kernel parameter vanishes. Within Recognition Science it connects the self-similar forcing chain (T5 J-uniqueness and T6 phi fixed point) to cosmological observables through the locked exponent. The limit and positivity results build directly upon it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.