GrowthODE_ILG
plain-language theorem explainer
GrowthODE_ILG encodes the predicate that a trial function D_func obeys the ILG-corrected growth equation a²D'' + (3/2)aD' - (3/2)w(a,k)D = 0 for a > 0 in an EdS background, with w supplied by the ILG kernel. Model builders checking approximate solutions to structure growth under Recognition Science corrections would invoke this predicate. The definition is a direct, one-line encoding of the second-order ODE using Mathlib's deriv operator and the imported kernel.
Claim. Let $w(a) = 1 + C_P (a/(k τ_{0,P}))^α_P$ (regularized at small argument). Then GrowthODE_ILG(P, k, D) holds precisely when, for every $a > 0$, $a^2 D''(a) + (3/2)a D'(a) - (3/2) w(a) D(a) = 0$, where primes denote derivatives with respect to scale factor $a$ and the parameters $C_P, τ_{0,P}, α_P$ are taken from the KernelParams record $P$.
background
KernelParams supplies the three ILG correction constants C, τ₀ and α that enter the kernel. The kernel itself is defined as w(P, k, a) = 1 + P.C · (max 0.01 (a/(k P.τ₀)))^P.α, recovering the constant kernel w = 1 when C = 0. In the EdS background the standard growth equation reduces to a²D'' + (3/2)aD' - (3/2)D = 0; the ILG version replaces the last coefficient by the scale-dependent factor w(a, k). The module works in the variable a (scale factor) rather than ln(a), producing the displayed second-order form.
proof idea
The declaration is a direct definition: it unfolds the kernel, substitutes into the displayed linear combination of second and first derivatives, and asserts that the combination vanishes identically for a > 0. No lemmas are applied; the body is the predicate itself.
why it matters
This predicate supplies the target equation against which the first-order ansatz D = a(1 + B a^α) is checked in the sibling declaration growth_satisfies_ode. It therefore closes the loop between the ILG kernel (imported from ILG.Kernel) and the approximate growth factor needed for structure-formation calculations in Recognition Science. The construction sits inside the broader ILG program that modifies the standard EdS growth ODE by the Recognition-derived kernel w.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.