SolvesModifiedPoisson
plain-language theorem explainer
SolvesModifiedPoisson defines the predicate that a potential Φ satisfies the modified Poisson equation -k²Φ = 4π kernel(P,k,a) δρ in Fourier space. Cosmologists studying ILG modifications cite this when verifying operator consistency with the kernel multiplier. The definition is a direct algebraic statement of the equation with no additional lemmas.
Claim. Let $w(k,a)$ be the ILG kernel with parameters $P$. Then Φ solves the modified Poisson equation when $-k^2 Φ = 4π w(k,a) δρ$.
background
The module defines the modified Poisson equation as a Fourier-space multiplier and proves basic stability bounds relative to standard GR. KernelParams is the structure holding the ILG parameters alpha (exponent), C (amplitude), and tau0 (reference scale). The kernel function is w(k,a) = 1 + C (a/(k tau0))^alpha, with a max safeguard at small arguments.
proof idea
Direct definition of the predicate as the equality -(k² Φ) = 4 π kernel(P,k,a) δρ. No lemmas or tactics are invoked; the body simply names the target equation.
why it matters
The predicate is invoked by the downstream theorem poisson_operator_solves to confirm that the operator definition satisfies the equation. It fills the Target A Poisson-with-kernel statement in the module, supplying the Fourier multiplier form used for later scaling and stability results relative to GR.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.