f_growth_eds_ilg
plain-language theorem explainer
This definition supplies the explicit formula for the logarithmic growth rate f = d ln D / d ln a of the density contrast in the ILG model on an Einstein-de Sitter background. Cosmologists computing linear structure growth or the integrated Sachs-Wolfe signal would cite the expression when comparing ILG corrections to standard GR. The formula is obtained by substituting the ansatz D = a (1 + B a^α) into the growth ODE and isolating the first derivative term.
Claim. Let $f(a,k;P)$ be the growth rate $dD/d a$ scaled by $a/D$. Then $f(a,k;P) = [1 + B(1+α)X^{-α}] / [1 + B X^{-α}]$, where $X = a/(k τ_0)$, $B$ is the growth prefactor built from $α$ and the ILG amplitude $C$, $α$ is the fine-structure constant, and $τ_0$ is the fundamental tick duration carried by the kernel parameters $P$.
background
In the ILG.GrowthODE module the linear growth factor satisfies the second-order ODE $D'' + (1/2)D' - (3/2)w(a,k)D = 0$ with independent variable ln a. The first-order ILG correction is introduced by the ansatz $D = a(1 + B a^α)$ whose prefactor $B$ is supplied by growth_prefactor. The present definition isolates the instantaneous growth rate $f = d ln D / d ln a$ from that ansatz. Upstream, tau0 is defined as the fundamental tick duration (both in Compat.Constants and Constants), alpha is the fine-structure constant, and the independent spatial semantics from LNALSemantics supply the voxel-level independence assumption underlying the kernel.
proof idea
The definition is a direct algebraic substitution. It first forms Xinv = a / (k * P.tau0), sets B := growth_prefactor P.alpha P.C, and returns the closed ratio (1 + B(1 + P.alpha) Xinv^P.alpha) / (1 + B Xinv^P.alpha). No external lemmas are applied; the expression follows immediately once the ansatz is differentiated with respect to ln a.
why it matters
The definition supplies the growth rate used by f_growth_gr_limit to recover the GR value 1 when C = 0 and by f_growth_gt_one to prove f > 1 for positive C. It is also the direct input to the ISW driver in ISWSign. Within the Recognition Science framework it encodes the first-order phi-ladder correction to the EdS growth equation that arises from the eight-tick octave and the RCL identity, thereby linking the kernel parameters to observable large-scale structure signals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.