poisson_operator_perturbation
plain-language theorem explainer
The poisson_operator_perturbation supplies the Fourier-space response of the ILG kernel to a density contrast δρ, with saturation below the cutoff wavenumber k_min. Researchers deriving perturbation growth in recognition-modified cosmologies cite this operator when separating background and fluctuation contributions. The definition evaluates to zero at k=0 and otherwise applies the bounded kernel_perturbation scaled by -4π δρ / k².
Claim. The perturbation Poisson operator is given by $Φ_pert(k) = 0$ if $k=0$, and $Φ_pert(k) = -4π w_pert(k_min,k,a) δρ / k²$ otherwise, where the infrared-bounded ILG kernel is $w_pert(k_min,k,a) = 1 + C (a / (max(k_min,k) τ_0))^α$ with parameters drawn from the KernelParams structure.
background
This module implements the modified Poisson equation in Fourier space for the ILG framework. The KernelParams structure bundles the ILG parameters: exponent α = (1 - 1/φ)/2, amplitude C, and reference timescale τ₀. The upstream kernel_perturbation function saturates the wavenumber at k_min for modes below the cutoff, yielding w_pert = 1 + C (a / (max(k_min,k) τ₀))^α. The local theoretical setting is the target of expressing the Poisson-with-kernel statement as a Fourier multiplier and establishing its stability relative to standard GR. Upstream results include the BIT kernel families and the base ILG kernel definition.
proof idea
The definition is a direct case distinction: it returns zero when k vanishes and otherwise multiplies the perturbation kernel by -4π δρ and divides by k². No lemmas are invoked; the expression is the explicit algebraic form of the operator.
why it matters
This definition supplies the fluctuation piece of the combined causality-bound Poisson operator, which is assembled in poisson_operator_full. It is invoked inside the master certificate CausalityBoundsPoissonCert to establish background independence and homogeneous-mode invariance. Within the Recognition framework it realizes the ILG modification of the Poisson equation while preserving the homogeneous FRW background, consistent with the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.