poisson_background_independent_of_kernel
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not bound the size of perturbation corrections.
- Does not treat time-dependent or nonlinear extensions.
- Does not derive numerical values inside the alpha band.
Lean usage
background_indep := poisson_background_independent_of_kernelformal statement (Lean)
94@[simp] theorem poisson_background_independent_of_kernel
95 (P : KernelParams) (a ρ_bar : ℝ) :
96 poisson_operator_full P 0 0 a ρ_bar 0
97 = poisson_operator_background a ρ_bar := by
proof body
Term-mode proof.
98 unfold poisson_operator_full poisson_operator_perturbation
99 simp
100
101/-- The perturbation kernel inside `poisson_operator_perturbation` is
102bounded above by its IR-saturated value. This is the operator-level
103restatement of `kernel_perturbation_bounded_above`: the multiplier in
104front of `δρ/k²` is uniformly bounded above by a finite ceiling fixed by
105the IR cutoff, so the perturbation operator does not run away as
106`k → 0`. -/