poisson_enhancement

formal source

  33
  34/-- Stability/Scaling Bound: The ILG potential Φ is strictly enhanced relative to
  35    the GR potential Φ_GR by exactly the kernel factor w(k, a). -/
  36theorem poisson_enhancement (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) :
  37    let Φ_ILG := poisson_operator P k a δρ
  38    let Φ_GR  := -(4 * Real.pi * δρ) / k^2
  39    |Φ_ILG| = kernel P k a * |Φ_GR| := by
  40  unfold poisson_operator
  41  simp only [if_neg hk]
  42  have h_kernel_pos : 0 < kernel P k a := kernel_pos P k a
  43  -- Rewrite -(4πw·δρ)/k² as w·(-(4π·δρ)/k²) under absolute value.
  44  have h_eq : -(4 * Real.pi * kernel P k a * δρ) / k^2
  45              = kernel P k a * (-(4 * Real.pi * δρ) / k^2) := by ring
  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