theorem
proved
term proof
poisson_coercive
show as:
view Lean formalization →
formal statement (Lean)
49theorem poisson_coercive (P : KernelParams) (k a δρ : ℝ) (hk : k ≠ 0) (hδρ : δρ ≠ 0) :
50 poisson_operator P k a δρ ≠ 0 := by
proof body
Term-mode proof.
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. -/