poisson_operator_solves
plain-language theorem explainer
The theorem verifies that the defined operator satisfies the modified Poisson predicate for any nonzero wavenumber. Workers on kernel-modified gravity models cite it to confirm the Fourier-space multiplier produces a valid potential from the density source. The proof is a direct term-mode reduction that unfolds both the predicate and operator, dispatches the k nonzero branch, and finishes with field simplification.
Claim. Let $P$ be a KernelParams bundle. For real $k,a,δρ$ with $k≠0$, the value $Φ=$poisson_operator$(P,k,a,δρ)$ obeys the modified Poisson relation $-k^2Φ=4π⋅kernel(P,k,a)⋅δρ$.
background
KernelParams bundles the ILG kernel constants: exponent α, amplitude C, and reference scale τ₀. The kernel function is defined as w(P,k,a)=1+C⋅(max(0.01,a/(kτ₀)))^α. SolvesModifiedPoisson is the predicate asserting that a candidate potential Φ satisfies the sourced equation -k²Φ=4π⋅w(P,k,a)⋅δρ. The module states its goal as expressing the modified Poisson equation via a Fourier-space multiplier and establishing basic stability bounds relative to GR.
proof idea
The term proof unfolds SolvesModifiedPoisson and poisson_operator, applies simp to the if_neg branch for hk:k≠0, introduces the auxiliary fact that k²≠0 via pow_ne_zero, and closes with field_simp to obtain the algebraic identity.
why it matters
The result discharges the central claim of Target A in the ILG.PoissonKernel module by confirming the operator solves the kernel-modified Poisson equation. It supplies the verified base case for the stability and scaling bounds developed in sibling declarations such as poisson_enhancement and poisson_coercive. The construction sits inside the broader ILG program that replaces the standard GR Poisson operator with a wavenumber-dependent multiplier drawn from the kernel families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.