CausalityBoundsPoissonCert
plain-language theorem explainer
The CausalityBoundsPoissonCert structure packages three identities confirming that the ILG-modified Poisson operator reduces exactly to the standard background solution whenever the density contrast vanishes. Workers on kernel-based cosmological perturbations cite it to guarantee that the background gravitational potential remains untouched by the kernel while perturbations are sourced only for inhomogeneous modes. Each identity follows by direct substitution into the operator definitions and case analysis on wavenumber.
Claim. The structure asserts three properties. For all kernel parameters $P$, scale factor $a$ and mean density $¯ρ$, the full operator at zero wavenumber and zero contrast equals the background operator: $poisson_operator_full(P,0,0,a,¯ρ,0)=poisson_operator_background(a,¯ρ)$. The perturbation operator vanishes at zero contrast: $poisson_operator_perturbation(P,k_min,k,a,0)=0$. The full operator at zero contrast equals the background for any wavenumber: $poisson_operator_full(P,k_min,k,a,¯ρ,0)=poisson_operator_background(a,¯ρ)$. Here $poisson_operator_background(a,¯ρ)=4π a² ¯ρ / 3$, the perturbation applies the kernel multiplier to $δρ$ with IR cutoff $k_min$, and the full operator is their sum.
background
The ILG.PoissonKernel module expresses the modified Poisson equation as a Fourier-space multiplier with explicit infrared cutoff and proves basic stability bounds relative to standard GR. The background operator is the standard FRW source term $4π a² ¯ρ / 3$ with no kernel dependence; its doc-comment states that the homogeneous mode sits at the J-cost minimum and does not source ledger gradient flow. The perturbation operator applies the kernel_perturbation factor to the density contrast $δρ$ only for $k>0$, saturating below $k_min=aH/c$ to remove the $k=0$ divergence. The full operator is defined as their direct sum. KernelParams supplies the RS-derived values $α=(1-1/φ)/2$, amplitude $C$ and reference scale $τ_0$.
proof idea
This is a structure definition that simply declares the three required identities as fields. No tactics appear inside the structure. The identities are discharged downstream by the three lemmas poisson_background_independent_of_kernel, poisson_operator_perturbation_homogeneous and poisson_operator_full_homogeneous, each obtained by unfolding the operator definitions and splitting on the case $k=0$.
why it matters
The structure supplies the master certificate for the causality-bound Poisson layer and is instantiated by the definition causalityBoundsPoissonCert. It anchors the ILG target of proving stability and scaling bounds for the Poisson-with-kernel statement relative to standard GR. The three properties ensure the kernel modification is confined to inhomogeneous modes, preserving the homogeneous background solution required by the Recognition Science forcing chain. No open scaffolding remains at this layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.