growth_satisfies_ode
plain-language theorem explainer
The closed-form growth factor D(a) = a(1 + B (a/(k τ₀))^α) satisfies the ILG-modified EdS growth ODE to first order in the correction parameter C. Cosmologists working with Recognition Science modifications to structure formation would cite the result when confirming that a trial solution remains consistent with the background dynamics. The proof proceeds by explicit differentiation of the ansatz, substitution of the kernel, and algebraic cancellation that isolates the controlled error term.
Claim. Let B denote the growth prefactor depending on α and C. Define the trial solution D(a) := a (1 + B (a/(k τ₀))^α). Then for a > 0 with a/(k τ₀) ≥ 0.01 the identity a² D''(a) + (3/2) a D'(a) − (3/2) w(a) D(a) + (3/2) C B (a/(k τ₀))^{2α} a = 0 holds, where w(a) is the ILG kernel at wavenumber k and τ₀ is the fundamental tick duration.
background
The ILG.GrowthODE module constructs the first-order correction to the EdS growth factor by inserting the power-law ansatz D(a) = a(1 + B a^α) into the background ODE. The prefactor B is supplied by the sibling definition growth_prefactor and is chosen to match the kernel source at linear order in C. The kernel function itself is imported from ILG.Kernel and encodes the Recognition Science modification to the Poisson equation on the phi-ladder. Upstream, τ₀ is the fundamental tick duration (defined as the RS-native time unit with positivity proved by direct comparison to the tick constant) and α is the fine-structure constant appearing in the exponent of the correction.
proof idea
The tactic proof first rewrites D using the prefactor definition and algebraic simplification of the power term. It computes the first derivative via the product and power rules, citing differentiability of rpow at positive arguments. The second derivative is obtained by differentiating the first-derivative expression inside a neighborhood filter. After unfolding the kernel and applying max-equality on the large-Xinv regime, field_simp and ring_nf reduce the left-hand side to the explicit error term, which is shown to cancel against the remaining contribution.
why it matters
This theorem supplies the consistency verification for the ILG growth ansatz inside the Recognition Science framework, allowing the closed-form solution to be used in downstream calculations of the matter power spectrum. It sits between the kernel definition and any application of the growth ODE to structure formation. The result fills the verification step required by the first-order ILG perturbation of the EdS background and touches the open question of extending the expansion to O(C²).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.