kernel_background_independent_of_params

formal source

 354homogeneous density does not source any ILG enhancement. This formalizes
 355the perturbation/background split that resolves Beltracchi's concern (2)
 356on the Lean side. -/
 357theorem kernel_background_independent_of_params (P : KernelParams) :
 358    kernel_background = 1 := rfl
 359
 360/-- **The mode partition.** For a density field `ρ = ρ̄ + δρ` with
 361homogeneous mean `ρ̄` and zero-mean fluctuation `δρ`, the ILG-modified
 362Poisson source decomposes as
 363\[ \rho_{\rm eff}(k,a) = \bar\rho \cdot k_{\rm bg} + \delta\rho(k) \cdot
 364  w_{\rm pert}(k_{\min}, k, a), \]
 365with the background factor `k_bg = 1` and the perturbation factor
 366saturated at `kernel_perturbation P k_min k_min a`. -/
 367noncomputable def mode_partition (P : KernelParams) (k_min k a ρ_bar δρ : ℝ) : ℝ :=
 368  ρ_bar * kernel_background + δρ * kernel_perturbation P k_min k a
 369
 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
 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. -/
 378theorem mode_partition_homogeneous (P : KernelParams) (k_min k a ρ_bar : ℝ) :
 379    mode_partition P k_min k a ρ_bar 0 = ρ_bar := by
 380  rw [mode_partition_eq]; ring
 381
 382/-! ### Dynamical-time form (no cumulative-time integration)
 383
 384The companion form for galactic systems is parameterized by the dynamical
 385time `T_dyn` of the orbit, never by cumulative cosmic time `t`. This
 386eliminates the literal Riemann–Liouville integral and resolves
 387Beltracchi's concern (1).