mode_partition_homogeneous
plain-language theorem explainer
The theorem establishes that the ILG mode partition returns exactly the background density when the density perturbation vanishes. Cosmologists working on homogeneous backgrounds in modified gravity frameworks would cite this to confirm absence of spurious enhancement in the unperturbed sector. The proof is a one-line wrapper that rewrites the mode partition definition and applies ring simplification.
Claim. For ILG kernel parameters $P$, minimum wave number $k_0$, wave number $k$, scale factor $a$, and background density $ρ_0$, the mode partition at zero perturbation satisfies mode_partition$(P, k_0, k, a, ρ_0, 0) = ρ_0$.
background
The ILG kernel takes the form $w(k,a)=1+C(a/(kτ_0))^α$ with $α=(1-1/φ)/2$, amplitude $C$, and reference tick $τ_0$. KernelParams is the structure bundling $α$, $C$, $τ_0$ together with the positivity condition $0<τ_0$ and nonnegativity of $α$. The module ILG.Kernel formalizes this kernel for galactic and cosmological applications, eliminating cumulative-time integrals in favor of dynamical time $T_dyn$. Upstream results supply the RS-native tick $τ_0=1$ and the BIT kernel families that reduce to the constant kernel when the perturbation vanishes.
proof idea
The proof is a one-line wrapper that rewrites via mode_partition_eq and then applies the ring tactic to obtain the required equality with the background density.
why it matters
This result is invoked inside causalityBoundsCert to certify that perturbations remain positive and bounded while the homogeneous mode stays unmodified. It completes the homogeneous case in the ILG kernel formalization, ensuring consistency with the Recognition Science forcing chain (T5 J-uniqueness through T8 $D=3$) and the Recognition Composition Law that fixes the self-similar exponent $α$. No open scaffolding remains on this specific equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.