kernel_with_Hubble_bounded_above
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.