poisson_operator_background
plain-language theorem explainer
The background Poisson operator supplies the standard FRW source term 4 π a² ρ_bar / 3 for the homogeneous density mode. Cosmologists separating background from kernel-modified perturbations in the ILG Poisson layer would cite this definition. It is supplied as a direct algebraic expression with no kernel dependence or ledger flow.
Claim. The background Poisson operator equals $4 π a^{2} ρ_bar / 3$, where $a$ is the scale factor and $ρ_bar$ the homogeneous density. This term sources the gravitational potential under the standard Poisson equation when the homogeneous mode sits at the J-cost minimum.
background
The module recasts the Poisson equation as a Fourier-space multiplier, with kernel modifications applied only to perturbations. The shifted cost H(x) = J(x) + 1 satisfies the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) under the Recognition Composition Law. The homogeneous mode ρ_bar produces no ledger gradient flow.
proof idea
Direct definition of the Newtonian source term. No lemmas or tactics are invoked; the expression is the standard FRW Poisson right-hand side for the homogeneous background.
why it matters
This definition supplies the homogeneous baseline inside poisson_operator_full and the master certificate CausalityBoundsPoissonCert. It isolates the standard FRW contribution so kernel effects act only on δρ, consistent with the T5 J-uniqueness and T8 D=3 landmarks. It closes the background-perturbation separation required by the Poisson-with-kernel target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.