kernel_with_Hubble
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove positivity or monotonicity properties of the kernel.
- Does not derive the exponent alpha from the phi ladder.
- Does not handle units where c is not equal to 1.
- Does not supply numerical evaluation for concrete parameter values.
formal statement (Lean)
260noncomputable def kernel_with_Hubble (P : KernelParams) (a H k : ℝ) : ℝ :=
proof body
Definition body.
261 kernel_perturbation P (a * H) k a
262
263/-- The perturbation kernel reduces to the original `kernel` when the
264 wavenumber is at or above the IR cutoff. -/