kernel_with_Hubble
plain-language theorem explainer
The declaration defines the Hubble-saturated ILG kernel by specializing the perturbation kernel to an infrared cutoff at the Hubble scale aH in units where c equals 1. Researchers modeling modified gravity or causal bounds in cosmology would reference this when applying the ILG framework to Hubble-horizon physics. It is implemented as a direct one-line wrapper around the perturbation kernel.
Claim. Let $P$ denote the ILG kernel parameters with exponent $alpha$, amplitude $C$, and reference timescale $tau_0 > 0$. The Hubble-saturated kernel for scale factor $a$, Hubble parameter $H$, and wavenumber $k$ is the perturbation kernel evaluated at minimum wavenumber $a H$.
background
The ILG kernel takes the form $w(k,a) = 1 + C (a / (k tau_0))^alpha$, with $alpha = (1 - 1/phi)/2$ from self-similarity. KernelParams is the structure holding these values together with the positivity requirement on $tau_0$. Upstream, the shifted cost function $H(x) = J(x) + 1$ converts the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. This module sits in the Infra-Luminous Gravity formalization, linking to BIT kernel families for cosmological applications.
proof idea
The definition is a one-line wrapper that invokes the perturbation kernel with the product a times H as the infrared cutoff wavenumber.
why it matters
This supplies the Hubble-saturated specialization needed for the master causality certificate, which establishes positivity, a lower bound of one, and upper boundedness by the value at k equals aH. It directly supports the Hubble ceiling theorem proving the bound. Within Recognition Science it realizes the infrared cutoff at the Hubble scale, aligning with the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.