poisson_enhancement
plain-language theorem explainer
The poisson_enhancement theorem states that the absolute value of the ILG Poisson potential equals the kernel factor times the absolute value of the GR potential for any nonzero wavenumber k. Cosmologists comparing kernel-corrected gravity to standard GR would cite this exact scaling when quantifying enhancement or stability. The short tactic proof unfolds the operator definition, invokes kernel positivity from the BIT family, rewrites the source term by ring algebra, and applies absolute-value multiplicativity.
Claim. Let $w(k,a)$ denote the BIT kernel evaluated at wavenumber $k$ and scale $a$. Let $Φ_{ILG}$ be the output of the modified Poisson operator on parameters $P$, $k$, $a$, and density contrast $δρ$. Let $Φ_{GR} = -4π δρ / k^2$. Then $|Φ_{ILG}| = w(k,a) · |Φ_{GR}|$.
background
The declaration lives in the ILG.PoissonKernel module whose module doc describes the target as a Fourier-space multiplier version of the Poisson equation together with basic stability and scaling bounds against GR. KernelParams supplies the parameter record for the operator; the kernel itself is imported from BITKernelFamilies and defined by cases (constant, 1/(1+z), or exponential decay). Upstream results include the kernel definition, the simplicial-to-continuum bridge that identifies the Laplacian action, and the forcing self-reference structure that supplies the overall consistency axioms.
proof idea
The tactic proof unfolds poisson_operator, simplifies the if-neg branch using hk : k ≠ 0, obtains kernel positivity via the imported kernel_pos lemma, rewrites the scaled GR term by a ring equality, then applies abs_mul and abs_of_pos to reach the exact scaling.
why it matters
This scaling supplies the precise enhancement factor required by the Poisson-with-kernel target statement in the ILG module. It closes the direct comparison to the GR baseline Φ_GR = -4π δρ / k² and thereby supports the broader Recognition Science claim that the kernel multiplier encodes the departure from standard gravity. No downstream uses are recorded yet; the result remains a foundational stability lemma inside the ILG development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.