kernel_perturbation_bounded_above
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not establish a matching lower bound on the kernel.
- Does not compute the kernel at specific physical wavenumbers.
- Does not derive the constants C or α from first principles.
- Applies only for positive k_min and a.
Lean usage
exact kernel_perturbation_bounded_above P hkmin ha kformal statement (Lean)
313theorem kernel_perturbation_bounded_above
314 (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min) {a : ℝ} (ha : 0 < a)
315 (k : ℝ) :
316 kernel_perturbation P k_min k a
317 ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
proof body
Tactic-mode proof.
318 unfold kernel_perturbation
319 -- max k_min k ≥ k_min, so 1/(max k_min k) ≤ 1/k_min, so
320 -- a/(max k_min k * tau0) ≤ a/(k_min * tau0).
321 have h_max_ge : k_min ≤ max k_min k := le_max_left _ _
322 have h_max_pos : 0 < max k_min k := lt_of_lt_of_le hkmin h_max_ge
323 have h_kmin_tau_pos : 0 < k_min * P.tau0 := mul_pos hkmin P.tau0_pos
324 have h_max_tau_pos : 0 < max k_min k * P.tau0 := mul_pos h_max_pos P.tau0_pos
325 have h_arg_le : a / (max k_min k * P.tau0) ≤ a / (k_min * P.tau0) := by
326 apply div_le_div_of_nonneg_left (le_of_lt ha) h_kmin_tau_pos
327 exact mul_le_mul_of_nonneg_right h_max_ge P.tau0_pos.le
328 -- Now max 0.01 is monotone, and rpow is monotone for positive base + nonneg exponent.
329 have h_max_le : max 0.01 (a / (max k_min k * P.tau0))
330 ≤ max 0.01 (a / (k_min * P.tau0)) := by
331 exact max_le_max (le_refl _) h_arg_le
332 have h_lhs_pos : 0 < max 0.01 (a / (max k_min k * P.tau0)) := by
333 apply lt_max_of_lt_left; norm_num
334 have h_rpow_le : (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
335 ≤ (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
336 apply Real.rpow_le_rpow (le_of_lt h_lhs_pos) h_max_le P.alpha_nonneg
337 have h_mul_le : P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
338 ≤ P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
339 exact mul_le_mul_of_nonneg_left h_rpow_le P.C_nonneg
340 linarith
341
342/-- **The Hubble ceiling theorem.** The Hubble-saturated kernel is bounded
343above by the value attained at the Hubble wavenumber `k = a H`. This is
344a specialization of `kernel_perturbation_bounded_above` to the canonical
345RS choice `k_min = a H / c`. -/