poisson_operator
plain-language theorem explainer
The poisson_operator supplies the explicit Fourier-space solution mapping a density perturbation δρ to the gravitational potential under the ILG kernel weighting. Cosmologists studying modified gravity or structure formation in ILG models cite this definition when constructing potentials from sources. It is realized as a direct conditional algebraic expression that scales the standard Poisson solution by the kernel factor w(k,a) while returning zero at vanishing wavenumber.
Claim. Let $w(k,a)$ be the ILG kernel. The operator is defined by $0$ when $k=0$, and by $-(4π w(k,a) δρ)/k^2$ otherwise. This realizes the Fourier-space relation $-k^2 Φ(k,a) = 4π w(k,a) δρ(k,a)$.
background
KernelParams bundles the ILG parameters α, C and τ₀. The kernel function is w(k,a) = 1 + C (max 0.01, a/(k τ₀))^α. This module expresses the modified Poisson equation as a Fourier-space multiplier and derives stability and scaling bounds relative to GR. Upstream, the ILG.Kernel.kernel supplies the explicit weighting w(k,a) that encodes the modification, while BITKernelFamilies.kernel provides comparison forms.
proof idea
One-line definition that directly encodes the algebraic solution to the modified Poisson equation. The body applies the kernel multiplier to the standard GR term -(4π δρ)/k² and inserts the zero case for k=0 to avoid division by zero.
why it matters
This definition is the core operator for the ILG Poisson kernel module and is invoked by poisson_coercive, poisson_enhancement and poisson_operator_solves. It fills the module target of stating the Poisson-with-kernel equation in Fourier space and supplies the mapping needed for the subsequent coercivity and enhancement bounds. In the Recognition framework it supports the ILG extension of gravitational dynamics consistent with kernel modifications from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.