kernel_at_ratio_one_alpha_zero
plain-language theorem explainer
The theorem shows that the ILG kernel equals 1 plus the amplitude constant C exactly when the scale ratio a over k tau0 is one and the exponent alpha is zero. Modelers of modified gravity at reference wavenumbers cite this reduction to recover the unmodified case. The proof unfolds the kernel definition, invokes the max property under the given ratio, and simplifies via the zero-exponent identity.
Claim. Let $P$ be an ILG kernel parameter bundle with exponent $α=0$, amplitude $C$, and reference time $τ_0$. For wavenumber $k≠0$ and scale factor $a$ satisfying $a/(k τ_0)=1$, the kernel satisfies $w(k,a)=1+C$.
background
The ILG kernel is defined by $w(k,a)=1+C·(max(0.01,a/(k τ_0)))^α$, where $α=(1-1/φ)/2$ is the self-similarity exponent and $C$ measures coercivity slack. KernelParams bundles these values together with the positivity constraint $0<τ_0$. The module formalizes the kernel as the central object linking scale-factor dependence to CPM coercivity constants.
proof idea
Unfold the kernel definition. Establish that max(0.01, a/(k·P.tau0)) equals 1 by rewriting the ratio hypothesis and applying max_eq_right. Finish with simp using the zero exponent, the max equality, and Real.rpow_zero.
why it matters
This supplies the reference-scale reduction of the ILG kernel when the exponent vanishes, recovering the constant-kernel limit required by the module's main results on positivity and monotonicity. It anchors the connection to CPM coercivity constants listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.