kernel_perturbation_eq_kernel_of_ge
plain-language theorem explainer
The equality shows that the IR-bounded ILG perturbation kernel equals the base kernel once the wavenumber meets or exceeds the cutoff. Cosmologists working with scale-dependent modifications in the infra-luminous regime cite this to drop the max operation for k greater than or equal to k_min. The term-mode proof unfolds both definitions and rewrites the max via a direct application of max_eq_right to the supplied inequality.
Claim. Let $P$ be an ILG kernel parameter bundle with exponent $α$, amplitude $C$, and reference scale $τ_0$. For real numbers $k_{min} ≤ k$ and scale factor $a$, the IR-perturbed kernel equals the base kernel: $1 + C (a / (max(k_{min}, k) τ_0))^α = 1 + C (a / (k τ_0))^α$.
background
The ILG kernel is the function $w(k, a) = 1 + C · (a / (k τ_0))^α$ where $α = (1 - 1/φ)/2$. The perturbation variant replaces the denominator wavenumber by max($k_{min}$, $k$) to enforce an infrared cutoff at the inverse recognition horizon. KernelParams bundles the explicit RS-derived values of $α$, $C$, and $τ_0$ together with the positivity hypothesis on $τ_0$. The module sets the kernel inside CPM coercivity calculations and references the Law of Existence for the underlying self-similarity.
proof idea
The term proof first unfolds the definitions of kernel_perturbation and kernel. It then introduces the auxiliary equality max $k_{min}$ $k$ = $k$ obtained from max_eq_right applied to the hypothesis $k_{min} ≤ k$, and finishes with a single rewrite that substitutes this equality into the unfolded expression.
why it matters
The result supplies the simplification step needed whenever the ILG kernel is evaluated away from the infrared cutoff, allowing direct use of the base kernel expression in high-wavenumber regimes. It closes a basic property of the perturbation construction introduced in the same module and supports the connection to the Recognition Composition Law through the exponent $α$. No downstream theorems are recorded yet, leaving the precise placement inside larger BITKernelFamilies calculations open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.