kernel_background
plain-language theorem explainer
The ILG background kernel is defined to be identically 1. Cosmologists working on the perturbation/background split in modified Poisson equations would cite this constant. It is introduced by direct definition with no computation or hypotheses.
Claim. The background kernel factor is defined by $k_{bg} := 1$.
background
The ILG.Kernel module formalizes the full kernel $w(k,a) = 1 + C (a/(k τ_0))^α$ with $α = (1-1/φ)/2$ derived from self-similarity. The background component isolates the homogeneous Friedmann-Robertson-Walker contribution, which sits at the J-cost minimum $J(1)=0$ with zero ledger gradient flow. The recognition operator is at equilibrium on a homogeneous state, producing no lag or enhancement, so the background Poisson equation remains unmodified standard GR.
proof idea
Direct definition assigning the constant 1.
why it matters
This definition supplies the background factor in the mode partition, which decomposes the ILG-modified Poisson source into $ρ_bar · 1 + δρ · w_pert$. It feeds kernel_background_eq_one, kernel_background_independent_of_params, mode_partition, and CausalityBoundsCert (the Beltracchi 2026 resolution structure). The split ensures the homogeneous density sources no ILG enhancement while perturbations remain positive and bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.