`causalityBoundsCert`

definition

show as: view math explainer →

module: IndisputableMonolith.ILG.Kernel
domain: ILG
line: 470 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.Kernel on GitHub at line 470.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 477  partition_homogeneous := mode_partition_homogeneous
 478  dyn_pos := kernel_dynamical_time_pos
 479  no_cumulative_growth := kernel_dynamical_time_stationary
 480
 481end ILG
 482end IndisputableMonolith

papers checked against this theorem

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