kernel_background
plain-language theorem explainer
The ILG background kernel equals the constant 1. Cosmologists modeling the homogeneous Friedmann-Robertson-Walker sector in modified gravity cite it as the unmodified baseline before adding perturbations. It is introduced by direct constant assignment with no computation or lemmas required.
Claim. The background kernel satisfies $k_{bg} := 1$.
background
The ILG kernel takes the form $w(k,a) = 1 + C (a/(k τ_0))^α$ with exponent $α = (1-1/φ)/2$ derived from self-similarity. The background component isolates the homogeneous density case where the recognition operator sits at equilibrium. This places the system at the J-cost minimum $J(1)=0$ with zero ledger gradient flow, so the background Poisson equation remains that of standard GR.
proof idea
Direct definition that assigns the real number 1.
why it matters
It supplies the background factor in mode_partition, which decomposes effective density into homogeneous and fluctuation parts. Downstream results kernel_background_independent_of_params and mode_partition_eq use it to confirm zero ILG enhancement on homogeneous modes. This formalizes the perturbation/background split that resolves Beltracchi's concern on the Lean side and aligns with the J-cost minimum at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.