poisson_coercive
plain-language theorem explainer
The coercivity theorem establishes that the ILG-modified Poisson operator yields a nonzero value whenever the wave number k and density perturbation δρ are both nonzero. Researchers modeling Fourier-space gravitational potentials with kernel cutoffs would cite this result to guarantee that sources produce nontrivial fields without accidental cancellation. The proof is a direct term-mode algebraic verification that unfolds the operator definition, confirms the kernel is positive, multiplies through the nonzero factors 4π and δρ, and divides by a
Claim. Let $P$ be KernelParams and let $k,a,δρ∈ℝ$ with $k≠0$ and $δρ≠0$. Then the modified Poisson operator $𝒫(P,k,a,δρ)≠0$.
background
The module defines the modified Poisson equation as a Fourier-space multiplier and proves basic stability and scaling bounds relative to standard GR. The kernel function (imported from BITKernelFamilies) supplies the IR cutoff that regularizes the $k→0$ divergence while the background FRW mode remains unmodified. The operator itself is the explicit multiplier $-(4π⋅kernel(P,k,a)⋅δρ)/k²$ that solves the sourced equation in Fourier space.
proof idea
The proof is a one-line wrapper that unfolds poisson_operator, applies simp to drop the conditional branch (using hk), then chains mul_ne_zero and div_ne_zero lemmas: k²≠0 follows from pow_ne_zero, 4π≠0 from norm_num and pi_ne_zero, kernel≠0 from kernel_pos.ne', the full numerator product is nonzero by successive multiplication, its negation is nonzero, and the final division by k² is therefore nonzero.
why it matters
This coercivity bound guarantees the modified potential is nontrivial for any nonzero source, forming part of the basic stability/scaling results that resolve Beltracchi's IR concern by splitting the Poisson system into an unmodified background piece and an ILG-perturbed piece. It supports the module's target of a self-consistent kernel-modified Poisson equation while preserving standard GR behavior for the homogeneous mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.