poisson_operator_perturbation_homogeneous
The declaration shows that the ILG-modified Poisson perturbation operator returns zero for vanishing density perturbation, establishing that the kernel modification leaves the homogeneous FRW background untouched. Researchers modeling ILG corrections to gravity or cosmology would cite this result to verify consistency with standard background evolution. The proof is a direct unfolding of the operator definition followed by case analysis on the wavenumber and simplification.
claimLet $P$ be an ILG kernel parameter set. For all real numbers $k_{min}$, $k$, $a$, the Fourier multiplier for the perturbed density term in the modified Poisson equation vanishes when the density contrast is zero: the operator applied to zero perturbation equals zero.
background
The module develops the Poisson-with-kernel formulation for ILG, expressing the modified Poisson equation via a Fourier-space multiplier that incorporates the ILG kernel. KernelParams bundles the RS-derived constants: the exponent alpha = (1 - 1/phi)/2, amplitude C, and reference timescale tau0. The upstream definition of the perturbation operator sets it to -(4 pi * kernel_perturbation(P, k_min, k, a) * delta_rho) / k^2 for k ≠ 0 and zero otherwise, with the canonical cutoff k_min = a H / c. This result is the operator-level statement of background-mode invariance under the ILG kernel.
proof idea
The proof unfolds the definition of the perturbation operator and splits into cases according to whether the wavenumber k equals zero. Simplification in each case, using that the perturbation amplitude is zero, immediately yields the identity.
why it matters in Recognition Science
This theorem supplies one of the three components of the CausalityBoundsPoissonCert, which certifies that the ILG kernel respects causality bounds in the Poisson sector. It is invoked directly in the proof that the full operator at zero perturbation reduces to the background operator. In the Recognition Science framework this confirms that the kernel modification does not disturb the homogeneous mode, consistent with the eight-tick octave and D=3 spatial dimensions derived from the forcing chain.
scope and limits
- Does not address non-zero density perturbations or scaling bounds.
- Does not derive the kernel_perturbation function itself.
- Does not connect to the full forcing chain T0-T8.
Lean usage
rw [poisson_operator_perturbation_homogeneous]formal statement (Lean)
118@[simp] theorem poisson_operator_perturbation_homogeneous
119 (P : KernelParams) (k_min k a : ℝ) :
120 poisson_operator_perturbation P k_min k a 0 = 0 := by
proof body
Term-mode proof.
121 unfold poisson_operator_perturbation
122 by_cases hk : k = 0
123 · simp [hk]
124 · simp [hk]
125
126/-- The full operator at zero perturbation reduces to the background. -/