f_growth
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 in Recognition Science
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.
scope and limits
- Does not prove that the rate exceeds one for positive inputs; that is shown in the positivity result.
- Does not establish the general-relativity limit of unity; that is handled by the limit theorem.
- Does not derive the functional form from the universal forcing axioms; it encodes the paper expression.
- Does not perform numerical evaluation or data fitting.
Lean usage
unfold f_growth beta_growth; simpformal statement (Lean)
102noncomputable def f_growth (a k tau0 : ℝ) : ℝ :=
proof body
Definition body.
103 let beta := beta_growth k tau0
104 let ba := beta * a ^ alphaLock
105 1 + (alphaLock / (1 + alphaLock)) * ba / (1 + ba)
106
107/-- f > 1 for positive β and a (ILG enhances growth rate). -/