kernel_background
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not depend on wave number, scale factor, or any KernelParams.
- Does not alter the standard GR Poisson equation for homogeneous modes.
- Does not incorporate amplitude C, exponent α, or causality bounds.
formal statement (Lean)
254@[simp] noncomputable def kernel_background : ℝ := 1
proof body
Definition body.
255