poisson_operator_background
The background Poisson operator supplies the standard FRW source term 4 pi a squared rho bar over 3 for the homogeneous density mode. Cosmologists constructing kernel-modified Poisson equations around FRW backgrounds cite it as the unperturbed baseline. The definition is a direct algebraic expression with no kernel factors or reduction steps.
claimThe background Poisson operator for scale factor $a$ and mean density $bar rho$ equals $frac{4 pi a^2 bar rho}{3}$.
background
The ILG module treats the Poisson equation as a Fourier-space multiplier, with kernel modifications applied only to density perturbations. The background term assumes the homogeneous mode sits at the J-cost minimum, where the shifted cost H(x) = J(x) + 1 equals 1 at the identity and sources no ledger gradient flow, recovering the standard Poisson equation of FRW cosmology. Upstream CostAlgebra.H reparametrizes the Recognition Composition Law into the d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
Direct definition returning the algebraic expression 4 * Real.pi * a^2 * rho_bar / 3. No lemmas or tactics are invoked.
why it matters in Recognition Science
This definition anchors the homogeneous baseline inside poisson_operator_full and the master certificate CausalityBoundsPoissonCert, which records background independence from kernel parameters. It isolates the unperturbed gravitational potential before ILG modifications are added via the BIT kernel, consistent with the module's target of a Poisson-with-kernel statement relative to standard GR.
scope and limits
- Does not incorporate any BIT kernel or Fourier multiplier.
- Does not depend on wavenumber k or IR cutoff k_min.
- Does not include perturbation density delta rho.
- Does not source ledger gradient flow from the homogeneous mode.
formal statement (Lean)
75noncomputable def poisson_operator_background (a ρ_bar : ℝ) : ℝ :=
proof body
Definition body.
76 4 * Real.pi * a^2 * ρ_bar / 3
77
78/-- The perturbation Poisson operator: ILG-modified with explicit IR
79cutoff `k_min`. Below `k_min` the kernel saturates at its IR-floor value,
80preventing the divergence at `k = 0`. The canonical RS choice for the
81cutoff is the Hubble wavenumber `k_min = a H / c`. -/