`causalityBoundsCert`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.ILG.Kernel on GitHub at line 470.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.