SolvesModifiedPoisson
SolvesModifiedPoisson defines the predicate asserting that a potential Φ satisfies the modified Poisson equation -k²Φ = 4π kernel(P,k,a) δρ in Fourier space. Cosmologists working on ILG models cite this predicate when verifying that their operators produce consistent solutions for kernel-weighted sources. The definition is introduced as a direct algebraic equality without additional lemmas.
claimThe predicate holds when $-k^2 Φ = 4π · kernel(P,k,a) · δρ$, where $P$ is the ILG kernel parameter bundle and kernel(P,k,a) denotes the ILG kernel function $1 + C · (a/(k τ₀))^α$.
background
The module states the modified Poisson equation as a Fourier-space multiplier and proves stability bounds relative to standard GR. KernelParams bundles the exponent α = (1 - 1/φ)/2, amplitude C, and reference timescale τ₀. The ILG kernel is defined as w(k,a) = 1 + C · (max 0.01 (a/(k τ₀)))^α. Upstream results supply the BIT kernel family (constant, inverse, exponential forms) and the ILG kernel implementation.
proof idea
The declaration is a direct definition of the predicate as the equality -(k² Φ) = 4 π kernel(P,k,a) δρ. No tactics or lemmas are applied inside the definition itself.
why it matters in Recognition Science
This predicate is the target equation used by the downstream theorem poisson_operator_solves, which confirms that the poisson_operator satisfies the modified Poisson condition. It fills the Poisson-with-kernel statement in the ILG module, connecting to kernel definitions in cosmology and supporting modified dynamics within the Recognition framework.
scope and limits
- Does not prove existence or uniqueness of solutions Φ.
- Does not derive specific numerical values for kernel parameters.
- Does not address nonlinear or time-dependent extensions of the equation.
- Does not compare the kernel form to observational data.
formal statement (Lean)
23def SolvesModifiedPoisson (P : KernelParams) (k a δρ Φ : ℝ) : Prop :=
proof body
Definition body.
24 - (k^2 * Φ) = 4 * Real.pi * kernel P k a * δρ
25
26/-- The operator definition satisfies the predicate. -/