poisson_operator_full_homogeneous

formal source

 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 : ℝ),
 138                      poisson_operator_full P 0 0 a ρ_bar 0
 139                        = poisson_operator_background a ρ_bar
 140  perturbation_homogeneous : ∀ (P : KernelParams) (k_min k a : ℝ),
 141                              poisson_operator_perturbation P k_min k a 0 = 0
 142  full_homogeneous : ∀ (P : KernelParams) (k_min k a ρ_bar : ℝ),
 143                      poisson_operator_full P k_min k a ρ_bar 0
 144                        = poisson_operator_background a ρ_bar
 145
 146noncomputable def causalityBoundsPoissonCert : CausalityBoundsPoissonCert where
 147  background_indep := poisson_background_independent_of_kernel
 148  perturbation_homogeneous := poisson_operator_perturbation_homogeneous
 149  full_homogeneous := poisson_operator_full_homogeneous
 150
 151end ILG
 152end IndisputableMonolith