pith. machine review for the scientific record. sign in
def definition def or abbrev

causalityBoundsCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 470noncomputable def causalityBoundsCert : CausalityBoundsCert where
 471  pert_pos := kernel_perturbation_pos

proof body

Definition body.

 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

depends on (11)

Lean names referenced from this declaration's body.