kernel_background_independent_of_params
plain-language theorem explainer
The ILG background kernel equals one for any parameter bundle of exponent, amplitude and reference timescale. Cosmologists separating homogeneous Friedmann backgrounds from scale-dependent enhancements would cite this result to confirm that the standard Poisson equation remains unmodified on large scales. The proof is a one-line reflexivity that follows directly from the constant definition of the background kernel.
Claim. The background kernel satisfies $k_{bg}=1$ for every parameter bundle $P= (α, C, τ_0)$ where $α=(1-1/φ)/2$.
background
The ILG kernel takes the form $w(k,a)=1+C·(a/(k τ_0))^α$ with $α=(1-1/φ)/2$. The background component isolates the homogeneous density contribution, which sits at the J-cost minimum $J(1)=0$ with zero ledger gradient flow. Upstream, kernel_background is defined as the constant 1 while kernel_perturbation supplies the fluctuation term with an IR cutoff at $k_{min}$.
proof idea
The proof is a one-line term that applies reflexivity to the definition of kernel_background, which is hard-coded as 1 and carries no dependence on the KernelParams structure.
why it matters
This theorem establishes the background/perturbation decomposition required for consistency with standard GR on homogeneous scales and directly addresses Beltracchi's concern (2) on the Lean side. It supports the module's main results on kernel reduction to unity at reference scales and positivity for physical ranges. In the Recognition Science setting it aligns with the J-cost minimum for homogeneous states and the separation of background from the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.