poisson_operator_background

formal source

  72The homogeneous mode `ρ̄` sits at the J-cost minimum and does not source
  73any ledger gradient flow, so the background gravitational potential is
  74sourced by the standard Poisson equation. -/
  75noncomputable def poisson_operator_background (a ρ_bar : ℝ) : ℝ :=
  76  4 * Real.pi * a^2 * ρ_bar / 3
  77
  78/-- The perturbation Poisson operator: ILG-modified with explicit IR
  79cutoff `k_min`. Below `k_min` the kernel saturates at its IR-floor value,
  80preventing the divergence at `k = 0`. The canonical RS choice for the
  81cutoff is the Hubble wavenumber `k_min = a H / c`. -/
  82noncomputable def poisson_operator_perturbation (P : KernelParams)
  83    (k_min k a δρ : ℝ) : ℝ :=
  84  if k = 0 then 0
  85  else -(4 * Real.pi * kernel_perturbation P k_min k a * δρ) / k^2
  86
  87/-- The combined causality-bound Poisson operator: background plus
  88perturbation, with the kernel acting only on the perturbation. -/
  89noncomputable def poisson_operator_full (P : KernelParams)
  90    (k_min k a ρ_bar δρ : ℝ) : ℝ :=
  91  poisson_operator_background a ρ_bar + poisson_operator_perturbation P k_min k a δρ
  92
  93/-- The background piece is independent of the kernel parameters. -/
  94@[simp] theorem poisson_background_independent_of_kernel
  95    (P : KernelParams) (a ρ_bar : ℝ) :
  96    poisson_operator_full P 0 0 a ρ_bar 0
  97      = poisson_operator_background a ρ_bar := by
  98  unfold poisson_operator_full poisson_operator_perturbation
  99  simp
 100
 101/-- The perturbation kernel inside `poisson_operator_perturbation` is
 102bounded above by its IR-saturated value. This is the operator-level
 103restatement of `kernel_perturbation_bounded_above`: the multiplier in
 104front of `δρ/k²` is uniformly bounded above by a finite ceiling fixed by
 105the IR cutoff, so the perturbation operator does not run away as