poisson_background_independent_of_kernel
plain-language theorem explainer
The background solution to the modified Poisson equation decouples from kernel parameters when perturbation inputs vanish. Cosmologists using ILG models cite this to justify treating the homogeneous background separately from kernel-dependent corrections in Fourier space. The proof is a direct unfolding of the full operator followed by simplification that cancels all kernel terms.
Claim. For any kernel parameters $P$ and real numbers $a, bar rho$, the full Poisson operator with vanishing perturbation density and kernel adjustment equals the background Poisson operator: $mathcal{P}_{text{full}}(P, 0, 0, a, bar rho, 0) = mathcal{P}_{text{background}}(a, bar rho)$.
background
The module defines the modified Poisson equation as a Fourier-space multiplier and proves stability and scaling bounds relative to standard GR. The BIT kernel function supplies the multiplier, taking constant, inverse-one-plus-z, or exponential forms. Upstream structures supply nuclear densities on phi-tiers and ledger factorizations that calibrate the J-cost underlying the operator.
proof idea
One-line wrapper that unfolds poisson_operator_full and poisson_operator_perturbation then applies simp to reduce directly to the background operator.
why it matters
Supplies the background_indep field for the causalityBoundsPoissonCert record in the same module. It closes the Poisson-with-kernel target by confirming the homogeneous background is kernel-independent, aligning with the Recognition Science forcing chain where background quantities occupy fixed phi-ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.