`ILGPrediction`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.CPMInstance on GitHub at line 212.

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

 209/-! ## Falsifiability Bounds -/
 210
 211/-- Structure recording falsifiable predictions for ILG. -/
 212structure ILGPrediction where
 213  /-- Predicted rotation curve enhancement factor -/
 214  enhancement : ℝ
 215  /-- Uncertainty bound -/
 216  uncertainty : ℝ
 217  /-- The enhancement is bounded by the kernel -/
 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.