poisson_operator_perturbation_kernel_bounded

formal source

 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`. -/
 107theorem poisson_operator_perturbation_kernel_bounded
 108    (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min)
 109    {a : ℝ} (ha : 0 < a) (k : ℝ) :
 110    kernel_perturbation P k_min k a
 111      ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha :=
 112  kernel_perturbation_bounded_above P hkmin ha k
 113
 114/-- **Background-mode invariance.** When the perturbation `δρ = 0` (pure
 115homogeneous configuration), the perturbation operator vanishes and only
 116the standard FRW background remains. This is the operator-level statement
 117that the ILG kernel does not affect the homogeneous mode. -/
 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
 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. -/
 127theorem poisson_operator_full_homogeneous
 128    (P : KernelParams) (k_min k a ρ_bar : ℝ) :
 129    poisson_operator_full P k_min k a ρ_bar 0
 130      = poisson_operator_background a ρ_bar := by
 131  unfold poisson_operator_full
 132  rw [poisson_operator_perturbation_homogeneous]
 133  ring
 134
 135/-- **Master certificate for the causality-bound Poisson layer.** -/
 136structure CausalityBoundsPoissonCert where
 137  background_indep : ∀ (P : KernelParams) (a ρ_bar : ℝ),