poisson_coercive

formal source

  46  rw [h_eq, abs_mul, abs_of_pos h_kernel_pos]
  47
  48/-- Coercivity Bound: The modified potential is non-vanishing for any non-vanishing source. -/
  49theorem poisson_coercive (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) (hδρ : δρ ≠ 0) :
  50    poisson_operator P k a δρ ≠ 0 := by
  51  unfold poisson_operator
  52  simp only [if_neg hk]
  53  have hk2 : (k^2 : ℝ) ≠ 0 := pow_ne_zero 2 hk
  54  have h4pi_ne : (4 * Real.pi : ℝ) ≠ 0 :=
  55    mul_ne_zero (by norm_num) Real.pi_ne_zero
  56  have hkern_ne : kernel P k a ≠ 0 := (kernel_pos P k a).ne'
  57  have hnum_ne : (4 * Real.pi * kernel P k a * δρ : ℝ) ≠ 0 :=
  58    mul_ne_zero (mul_ne_zero h4pi_ne hkern_ne) hδρ
  59  have hneg_ne : -(4 * Real.pi * kernel P k a * δρ : ℝ) ≠ 0 := neg_ne_zero.mpr hnum_ne
  60  exact div_ne_zero hneg_ne hk2
  61
  62/-! ## Causality-bound Poisson operators (Beltracchi 2026 resolution)
  63
  64The original `poisson_operator` above is preserved unchanged. The two
  65operators below split the Poisson equation into a background piece
  66(unmodified standard GR) and a perturbation piece (ILG-modified, with the
  67IR cutoff that prevents the `k → 0` divergence). Together they form a
  68self-consistent ILG Poisson system that resolves Beltracchi's IR concern.
  69-/
  70
  71/-- The background Poisson operator: standard FRW, no ILG modification.
  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,