poisson_operator_full_homogeneous
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address nonzero density perturbations.
- Does not derive the explicit kernel multiplier form.
- Does not include time-dependent or relativistic corrections.
- Does not supply numerical deviation bounds for small perturbations.
Lean usage
example (P : KernelParams) (k_min k a ρ_bar : ℝ) : poisson_operator_full P k_min k a ρ_bar 0 = poisson_operator_background a ρ_bar := poisson_operator_full_homogeneous P k_min k a ρ_barformal statement (Lean)
127theorem poisson_operator_full_homogeneous
128 (P : KernelParams) (k_min k a ρ_bar : ℝ) :
129 poisson_operator_full P k_min k a ρ_bar 0
130 = poisson_operator_background a ρ_bar := by
proof body
Term-mode proof.
131 unfold poisson_operator_full
132 rw [poisson_operator_perturbation_homogeneous]
133 ring
134
135/-- **Master certificate for the causality-bound Poisson layer.** -/