kernel_perturbation_pos
plain-language theorem explainer
kernel_perturbation_pos establishes that the perturbation term inside the ILG kernel stays strictly positive for every admissible parameter bundle and every real wave number and scale factor. Cosmologists and gravity modelers cite it when confirming that the effective kernel never crosses zero in the infrared regime. The tactic proof unfolds the explicit formula, invokes nonnegativity of real powers, and finishes with linear arithmetic.
Claim. Let $P$ be a KernelParams bundle containing exponent $alpha geq 0$, amplitude $C geq 0$ and reference scale $tau_0 > 0$. For any real numbers $k_{min}$, $k$ and scale factor $a$, the perturbation term satisfies $0 < C cdot left( max left( 0.01, frac{a}{max(k_{min},k) tau_0} right) right)^{alpha}$.
background
The ILG kernel is written $w(k,a) = 1 + C (a/(k tau_0))^alpha$ where $alpha = (1-1/phi)/2$ is taken from self-similarity. KernelParams packages the triple $(alpha, C, tau_0)$ together with the sign constraints $tau_0 > 0$ and $C geq 0$. Upstream, tau0 is imported as the fundamental tick duration from Constants and from Compat.Constants; the BITKernelFamilies module supplies the base kernel shapes that this perturbation augments.
proof idea
The proof unfolds kernel_perturbation, applies lt_max_of_lt_left after norm_num to obtain positivity of the base, invokes Real.rpow_nonneg to obtain nonnegativity of the power, multiplies by the nonnegative C via mul_nonneg, and closes with linarith.
why it matters
The result is invoked directly inside causalityBoundsCert as the pert_pos field that certifies the full set of causality bounds for the ILG kernel. It supplies the positivity half of the well-posedness statement required by the module, which itself rests on the self-similar fixed-point construction and the eight-tick octave of the Recognition Science forcing chain. No open scaffolding remains for this particular claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.