kernel_eq_one_of_C_zero
plain-language theorem explainer
When the amplitude constant C vanishes in the ILG parameter bundle, the kernel function equals unity for arbitrary wavenumber k and scale factor a. Modelers of infra-luminous gravity corrections cite this reduction to recover unmodified Friedmann dynamics in the baseline limit. The proof is a direct term-mode simplification that substitutes the hypothesis into the kernel definition.
Claim. Let $w(k,a)$ be the ILG kernel $1 + C · (max(0.01, a/(k τ₀)))^α$ where the parameters α, C, τ₀ come from the KernelParams structure with τ₀ > 0. If C = 0 then $w(k,a) = 1$ for all real k, a.
background
The ILG kernel is defined in this module as w(k, a) = 1 + C · (max 0.01 (a / (k τ₀)))^α, with α = (1 - 1/φ)/2 drawn from self-similarity. KernelParams is the structure bundling alpha, C, tau0 together with the positivity condition tau0_pos : 0 < tau0. The module documentation states that the kernel reduces to 1 at the reference scale and connects to CPM coercivity constants.
proof idea
The proof is a one-line term-mode wrapper that applies simp to the kernel definition and the hypothesis C = 0, yielding the constant 1 directly.
why it matters
This theorem supplies the baseline case for the ILG kernel, confirming that the modification vanishes exactly when C = 0. It supports the module's listed main results on kernel positivity and reduction at reference scales. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.