kernel_perturbation_bounded_above
plain-language theorem explainer
The IR boundedness theorem asserts that for any KernelParams P, positive IR cutoff k_min and scale factor a, the perturbation kernel at wavenumber k satisfies w_pert(k_min, k, a) ≤ 1 + C (max(0.01, a/(k_min τ₀)) )^α. Cosmologists and formalizers of infra-luminous gravity cite this to prevent kernel runaway as k → 0. The proof is a direct monotonicity argument that reduces the general case to the saturated value at k = k_min via comparisons on the max and real power functions.
Claim. Let P be a KernelParams structure with amplitude C, exponent α ≥ 0, and reference timescale τ₀ > 0. For k_min > 0, a > 0, and any real k, the perturbation kernel obeys w_pert(k_min, k, a) ≤ 1 + C ⋅ (max(0.01, a/(k_min τ₀)) )^α.
background
The ILG kernel is defined as w(k, a) = 1 + C (a / (k τ₀))^α where α = (1 - 1/φ)/2 derives from self-similarity and C is the coercivity amplitude. KernelParams bundles these constants with positivity proofs for τ₀ and nonnegativity for α. This theorem sits inside the ILG.Kernel module whose main results include positivity, monotonicity, and reduction to unity at the reference scale a = k τ₀. Upstream, the reference timescale τ₀ comes from Constants.tick.
proof idea
The proof unfolds kernel_perturbation then establishes a chain of inequalities. It shows max(k_min, k) ≥ k_min so a/(max(k_min,k) τ₀) ≤ a/(k_min τ₀). Monotonicity of max(0.01, ·) and of rpow for positive base and nonnegative exponent yields the bound on the powered term. Multiplication by nonnegative C and linarith close the argument.
why it matters
This result supplies the IR boundedness certificate used in causalityBoundsCert and the Poisson operator perturbation bound. It directly addresses the homogeneous mode runaway concern by fixing a finite ceiling determined by the recognition horizon τ₀. In the broader framework it supports controlled behavior across scales. The parent theorems are kernel_with_Hubble_bounded_above and poisson_operator_perturbation_kernel_bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.