SolvesModifiedPoisson
plain-language theorem explainer
SolvesModifiedPoisson encodes the predicate that a potential Φ satisfies the modified Poisson equation -k²Φ = 4π w(P,k,a) δρ in Fourier space, with w the ILG kernel. Cosmologists stating kernel-modified gravity equations would cite this predicate to assert that a candidate Φ meets the sourced relation. The definition is a direct equational statement of the multiplier form.
Claim. The predicate that a scalar field $Φ$ satisfies the modified Poisson equation $-k^2 Φ = 4π · w(P,k,a) · δρ$, where $w$ is the ILG kernel function determined by the parameter bundle $P = (α, C, τ_0)$.
background
The module states its target as the Poisson-with-kernel formulation, expressing the modified Poisson equation via a Fourier-space multiplier and establishing basic stability and scaling bounds relative to standard GR. KernelParams bundles the exponent α = (1 - 1/φ)/2, amplitude C, and reference timescale τ₀ carrying RS-derived values. The ILG kernel is defined as w(k,a) = 1 + C · (a / (k τ₀))^α, with a max(0.01,·) guard. Upstream, the BIT kernel supplies alternative functional forms (constant, 1/(1+z), exponential).
proof idea
The declaration is the direct definition of the predicate as the algebraic equality -(k² Φ) = 4 π kernel(P,k,a) δρ. No lemmas or tactics are invoked; the body is the equational encoding itself.
why it matters
This predicate supplies the target equation verified by the downstream theorem poisson_operator_solves, which confirms that the defined operator meets the modified Poisson condition. It realizes the Target A statement of the module for the Poisson-with-kernel formulation inside the ILG setting, supporting subsequent stability bounds relative to GR.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.