kernel_perturbation
plain-language theorem explainer
The declaration defines the IR-bounded ILG perturbation kernel by saturating the wavenumber at k_min inside the standard kernel formula. Cosmologists modeling modified Poisson equations for density perturbations cite it to enforce a finite infrared cutoff tied to the recognition horizon. The definition is a direct algebraic expression that applies max to enforce the floor and a safety bound of 0.01.
Claim. The IR-bounded perturbation kernel is given by $w(k_min, k, a) = 1 + C · (max(0.01, a / (max(k_min, k) · τ₀)))^α$, where the parameter bundle supplies α = (1 − 1/φ)/2, amplitude C, and reference time τ₀.
background
The ILG kernel module formalizes the perturbation to the homogeneous background kernel w(k, a) = 1 + C · (a / (k τ₀))^α. Here k is wavenumber, a scale factor, τ₀ the reference tick duration, and α the exponent fixed by self-similarity. KernelParams is the structure holding these values together with positivity proofs on τ₀ and non-negativity on α.
proof idea
One-line definition that substitutes the saturated wavenumber max(k_min, k) into the base kernel expression and inserts the floor 0.01 inside the power.
why it matters
This definition supplies the concrete object used by kernel_perturbation_eq_kernel_of_ge, kernel_perturbation_at_IR_floor, kernel_perturbation_bounded_above, and the CausalityBoundsCert structure. It implements the infrared cutoff required to keep the ILG enhancement finite as k → 0, closing the background/perturbation split in the Recognition Science treatment of the Poisson equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.