`ilg_falsifiable_bound`

proved

show as: view math explainer →

module: IndisputableMonolith.ILG.CPMInstance
domain: ILG
line: 221 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.CPMInstance on GitHub at line 221.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

kernel IndisputableMonolith.Cosmology.BITKernelFamilies
kernel IndisputableMonolith.ILG.Kernel
kernel_ge_one IndisputableMonolith.ILG.Kernel
KernelParams IndisputableMonolith.ILG.Kernel

formal source

 218  enhancement_bounded : enhancement ≤ 2
 219
 220/-- The ILG kernel provides a falsifiable upper bound on dark matter effects. -/
 221theorem ilg_falsifiable_bound (P : KernelParams) (k a : ℝ) :
 222    kernel P k a ≥ 1 := kernel_ge_one P k a
 223
 224end ILG
 225end IndisputableMonolith

papers checked against this theorem

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