mode_partition
plain-language theorem explainer
The mode partition decomposes the effective ILG density source into an unmodified homogeneous background term and a fluctuation term scaled by the perturbation kernel. Cosmologists deriving mode-specific corrections to the Poisson equation in infra-luminous gravity models would cite this split when separating mean and fluctuating contributions. The definition is a direct linear combination of the constant background kernel and the IR-bounded perturbation kernel.
Claim. For kernel parameters $P$, infrared cutoff $k_0$, wavenumber $k$, scale factor $a$, mean density $bar rho$, and fluctuation $delta rho$, the partitioned source equals $bar rho + delta rho times w_pert(P, k_0, k, a)$, where $w_pert = 1 + C (a / (max(k_0, k) tau_0))^alpha$ with $alpha = (1 - 1/phi)/2$.
background
The ILG kernel module defines the modification factor $w(k,a) = 1 + C (a/(k tau_0))^alpha$ with exponent $alpha = (1-1/phi)/2$ drawn from self-similarity. KernelParams is the structure holding this exponent, the amplitude $C$, and the reference timescale $tau_0 > 0$. The background kernel is identically 1, as the homogeneous FRW state sits at the J-cost minimum with zero ledger gradient. The perturbation kernel caps the enhancement below the infrared cutoff $k_min$ (the inverse recognition horizon) by replacing $k$ with $max(k_min, k)$ inside the power.
proof idea
One-line definition that multiplies the mean density by the background kernel (equal to 1) and the fluctuation by the perturbation kernel.
why it matters
This decomposition supplies the source term for the master causality certificate and the equality and homogeneous-mode theorems in the same module. It isolates the scale-dependent ILG correction while leaving the background Poisson equation unmodified, consistent with equilibrium on homogeneous states. The construction supports the recognition composition law and the eight-tick octave by keeping the homogeneous mode at the J-cost zero point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.