kernel_with_Hubble_bounded_above
The Hubble ceiling theorem bounds the ILG kernel at the Hubble wavenumber from above by 1 plus the amplitude C times a clipped ratio of scale factor to Hubble time raised to the exponent alpha. Cosmologists certifying perturbation bounds in Recognition Science would cite this to close the causality certificate. The proof is a one-line wrapper that unfolds the Hubble kernel definition and invokes the general perturbation bound after confirming positivity of the product a H.
claimLet $P$ be an ILG kernel parameter bundle containing exponent $alpha$, amplitude $C$, and reference timescale $tau_0 > 0$. For scale factor $a > 0$ and Hubble parameter $H > 0$, the Hubble-saturated kernel satisfies $w(k,a,H) leq 1 + C left( max(0.01, a/(a H tau_0)) right)^alpha$ for any wavenumber $k$.
background
The ILG kernel takes the form $w(k,a) = 1 + C cdot (a/(k tau_0))^alpha$, with $alpha = (1 - 1/phi)/2$ fixed by self-similarity and $tau_0$ the fundamental tick duration from the Constants module. KernelParams packages these quantities together with explicit positivity of $tau_0$ and nonnegativity of $alpha$ to guarantee the expression is well-defined for physical ranges. The module formalizes the perturbation/background split, stating that the homogeneous density does not source any ILG enhancement.
proof idea
The proof unfolds the definition of the Hubble kernel and applies the general perturbation bound lemma after confirming positivity of the product a H. It is a one-line wrapper that specializes the prior result to the canonical choice k_min = a H.
why it matters in Recognition Science
This theorem supplies the Hubble-specific case required by the causalityBoundsCert, which assembles positivity, monotonicity, and boundedness into a single inhabited certificate. It completes the formalization of the ILG kernel at cosmological scales and connects directly to the perturbation/background split that resolves Beltracchi's concern on the Lean side. The result sits inside the broader ILG development that links to the Recognition Composition Law and the phi-derived constants.
scope and limits
- Does not establish lower bounds or equality cases for the kernel.
- Does not apply when a or H fail to be positive.
- Does not incorporate quantum or higher-order corrections.
- Does not fix numerical values for C or alpha beyond the parameter bundle.
Lean usage
example (P : KernelParams) (a H k : ℝ) (ha : 0 < a) (hH : 0 < H) : kernel_with_Hubble P a H k ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha := kernel_with_Hubble_bounded_above P ha hH kformal statement (Lean)
346theorem kernel_with_Hubble_bounded_above
347 (P : KernelParams) {a H : ℝ} (ha : 0 < a) (hH : 0 < H) (k : ℝ) :
348 kernel_with_Hubble P a H k
349 ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha := by
proof body
Term-mode proof.
350 unfold kernel_with_Hubble
351 exact kernel_perturbation_bounded_above P (mul_pos ha hH) ha k
352
353/-- The background mode is independent of every kernel parameter: the
354homogeneous density does not source any ILG enhancement. This formalizes
355the perturbation/background split that resolves Beltracchi's concern (2)
356on the Lean side. -/