poisson_operator_full_homogeneous
plain-language theorem explainer
The theorem shows that the ILG-modified full Poisson operator, when the density perturbation vanishes, reduces exactly to the standard FRW background operator. Cosmologists verifying kernel corrections to gravitational potentials would cite it to confirm homogeneous modes remain unaffected by the ILG kernel. The proof is a one-line algebraic reduction that unfolds the full operator definition, applies the homogeneous perturbation vanishing result, and simplifies by ring.
Claim. Let $P$ be the kernel parameter bundle with RS-derived constants, and let $k_{min},k,a,bar rho$ be real numbers. Then the full Poisson operator $mathcal P_{full}(P,k_{min},k,a,bar rho,0)$ equals the background operator $mathcal P_{background}(a,bar rho)=frac{4pi a^2 bar rho}{3}$.
background
The module formulates the modified Poisson equation in Fourier space as a multiplier with an ILG kernel that saturates below an infrared cutoff to enforce causality. The background operator is the unmodified FRW term $4pi a^2 bar rho/3$, which sources the potential when the homogeneous mode sits at the J-cost minimum and produces no ledger gradient. KernelParams packages the explicit RS values alpha=(1-1/phi)/2, amplitude C, and reference timescale tau_0.
proof idea
The proof is a one-line wrapper. It unfolds the definition of the full operator as background plus perturbation, rewrites the perturbation term via the homogeneous invariance theorem that sets it to zero at zero density contrast, and finishes with ring simplification.
why it matters
This result supplies the final homogeneous reduction needed for the downstream causalityBoundsPoissonCert that bundles background independence, perturbation vanishing, and the full homogeneous case. It directly advances the module target of stability and scaling bounds for the kernel-modified Poisson equation relative to standard GR. In the Recognition framework it confirms the ILG kernel leaves the homogeneous mode invariant, consistent with the J-cost minimum and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.