kernel_perturbation_at_IR_floor
plain-language theorem explainer
The theorem establishes that the ILG perturbation kernel equals the base kernel evaluated at the infrared floor wavenumber when the input wavenumber lies at or below that floor. Cosmologists and gravity modelers working with scale-dependent kernels would cite this to simplify infrared-regularized expressions. The proof is a direct term reduction that unfolds both kernel definitions and substitutes the max-equality fact under the floor hypothesis.
Claim. Let $P$ be an ILG kernel parameter structure with exponent $alpha$, amplitude $C$, and reference timescale $tau_0$. For real wavenumbers $k_{min}$ and $k$ satisfying $k leq k_{min}$, and scale factor $a$, the perturbation kernel satisfies $w_{pert}(P, k_{min}, k, a) = w(P, k_{min}, a)$.
background
The ILG kernel formalization defines the base function as $w(k,a) = 1 + C cdot (max(0.01, a/(k tau_0)))^alpha$, where $alpha = (1-1/phi)/2$ is the self-similar exponent. KernelParams is the structure bundling $alpha$, $C$, $tau_0$ together with the positivity and nonnegativity hypotheses required for the expression to be well-defined. The local setting is the Infra-Luminous Gravity kernel inside the Recognition Science framework, which supplies the functional form used for perturbation expansions around the reference scale.
proof idea
The term proof unfolds the definitions of kernel_perturbation and kernel, introduces the auxiliary equality max k_min k = k_min via max_eq_left under the hypothesis k leq k_min, and rewrites the expression to obtain the stated equality.
why it matters
This result supplies the infrared boundary case for the ILG kernel, ensuring the perturbation expression collapses cleanly at the floor wavenumber. It supports consistent reduction in downstream cosmological and mechanism-design applications that rely on the kernel. The equality aligns with the Recognition Science phi-derived exponent and the eight-tick octave structure already encoded in the KernelParams bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.