 4438. The dynamical-time kernel is constant for a stationary orbit (no `t^α`
 444   growth).
 445-/
 446structure CausalityBoundsCert where
 447  pert_pos : ∀ (P : KernelParams) (k_min k a : ℝ),
 448              0 < kernel_perturbation P k_min k a
 449  pert_ge_one : ∀ (P : KernelParams) (k_min k a : ℝ),
 450                 1 ≤ kernel_perturbation P k_min k a
 451  IR_bounded : ∀ (P : KernelParams) (k_min : ℝ), 0 < k_min →
 452                 ∀ (a : ℝ), 0 < a →
 453                 ∀ (k : ℝ),
 454                 kernel_perturbation P k_min k a
 455                   ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha
 456  Hubble_bounded : ∀ (P : KernelParams) (a H : ℝ), 0 < a → 0 < H →
 457                    ∀ (k : ℝ),
 458                    kernel_with_Hubble P a H k
 459                      ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha
 460  background_eq_one : kernel_background = 1
 461  partition_homogeneous : ∀ (P : KernelParams) (k_min k a ρ_bar : ℝ),
 462                          mode_partition P k_min k a ρ_bar 0 = ρ_bar
 463  dyn_pos : ∀ (P : KernelParams) (T_dyn : ℝ),
 464             0 < kernel_dynamical_time P T_dyn
 465  no_cumulative_growth : ∀ (P : KernelParams) (T_dyn _t1 _t2 : ℝ),
 466                          kernel_dynamical_time P T_dyn
 467                            = kernel_dynamical_time P T_dyn
 468
 469/-- The causality-bound certificate is inhabited. -/
 470noncomputable def causalityBoundsCert : CausalityBoundsCert where
 471  pert_pos := kernel_perturbation_pos
 472  pert_ge_one := kernel_perturbation_ge_one
 473  IR_bounded := fun P k_min hkmin a ha k =>
 474    kernel_perturbation_bounded_above P hkmin ha k
 475  Hubble_bounded := fun P a H ha hH k => kernel_with_Hubble_bounded_above P ha hH k
 476  background_eq_one := kernel_background_eq_one

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.