mode_partition_eq
plain-language theorem explainer
The equality decomposes the mode partition into background density plus contrast scaled by the kernel perturbation. Cosmologists applying infra-luminous gravity corrections to density modes would cite this when separating homogeneous and inhomogeneous contributions. The proof is a direct term-mode reduction that unfolds the partition and background definitions then normalizes via ring.
Claim. Let $P$ be the kernel parameter bundle containing exponent $(1-1/φ)/2$, amplitude $C$, and reference scale $τ_0$. For real numbers $k_{min}$, $k$, $a$, background density $ρ_bar$, and contrast $δρ$, the partitioned mode density equals $ρ_bar + δρ$ times the kernel perturbation factor evaluated at those arguments.
background
The ILG kernel takes the form $w(k,a)=1+C(a/(kτ_0))^α$ with $α=(1-1/φ)/2$. KernelParams is the structure that packages this exponent, the amplitude $C$, the reference time $τ_0>0$, and the non-negativity of $α$. The mode partition function combines the background density with the contrast modulated by this kernel. The module formalizes infra-luminous gravity corrections to standard cosmology, with the kernel reducing to unity at the reference scale. Upstream structures supply nuclear densities on φ-tiers and ledger factorizations that calibrate the underlying J-cost.
proof idea
The proof is a one-line term wrapper. It unfolds the definitions of the mode partition and the kernel background, then applies the ring tactic to obtain the algebraic identity.
why it matters
The result supplies the explicit decomposition invoked by the homogeneous-mode theorem, which states that the partition collapses to the background density when the contrast vanishes. It fills the basic algebraic step in the ILG kernel formalization, consistent with the self-similar forcing chain and the J-uniqueness property that fixes the exponent. No open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.