kernel_with_Hubble
plain-language theorem explainer
The Hubble-saturated kernel specializes the ILG perturbation kernel by fixing the infrared cutoff at the Hubble wavenumber aH in units with c=1. Cosmologists deriving causality bounds or IR cutoffs in modified gravity models cite this specialization. It is a one-line definition that substitutes the cutoff directly into kernel_perturbation.
Claim. Define the Hubble-saturated kernel by $w_H(P,a,H,k) :=$ perturbation kernel evaluated at infrared cutoff $k_min = aH$, where $P$ is the parameter bundle holding exponent $alpha = (1-1/phi)/2$, amplitude $C$, and reference scale $tau_0 > 0$.
background
KernelParams bundles the ILG parameters: exponent alpha derived from self-similarity, amplitude C tied to coercivity slack, and reference time tau0 with positivity proof. The module formalizes the base ILG kernel as w(k,a) = 1 + C (a/(k tau0))^alpha. The perturbation kernel extends this form to an arbitrary infrared cutoff k_min while preserving positivity and monotonicity in scale factor a. Upstream, H from CostAlgebra supplies the shifted J-cost satisfying the d'Alembert form of the Recognition Composition Law, and the BIT kernel supplies the constant, inverse, and exponential families used in the broader cosmology layer.
proof idea
One-line wrapper that applies kernel_perturbation to the Hubble cutoff a*H while passing the remaining arguments a and k unchanged.
why it matters
This definition supplies the canonical infrared cutoff choice k_min = aH required by the master causality certificate and by the Hubble ceiling theorem. The certificate lists IR boundedness and the Hubble ceiling as two of its eight proved clauses; the ceiling theorem then specializes the general perturbation bound to this cutoff. It closes the step from the abstract ILG kernel to the concrete Hubble-saturated form used in expanding-universe bounds, consistent with the eight-tick octave and D=3 spatial structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.