mode_partition_eq
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the explicit functional form of the kernel perturbation.
- Does not prove positivity or monotonicity of the kernel.
- Does not address time integration or cumulative effects.
- Does not connect the equality to specific observational data.
Lean usage
rw [mode_partition_eq]; ringformal statement (Lean)
370theorem mode_partition_eq (P : KernelParams) (k_min k a ρ_bar δρ : ℝ) :
371 mode_partition P k_min k a ρ_bar δρ
372 = ρ_bar + δρ * kernel_perturbation P k_min k a := by
proof body
Term-mode proof.
373 unfold mode_partition kernel_background; ring
374
375/-- **Background mode of the partition is unmodified.** When `δρ = 0`,
376the effective source equals the background source — no ILG enhancement
377on the homogeneous mode. -/