`Falsifiers`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.ILG.Falsifiers
domain: Relativity
line: 8 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.ILG.Falsifiers on GitHub at line 8.

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

used by

formal source

   5namespace ILG
   6
   7/-- Enumerate falsifier bands for ILG (PPN, lensing, GW). -/
   8structure Falsifiers where
   9  ppn_tight    : ℝ
  10  lensing_band : ℝ
  11  gw_band      : ℝ
  12  deriving Repr
  13
  14/-- Predicate that falsifier bands are nonnegative (admissible). -/
  15def falsifiers_ok (f : Falsifiers) : Prop :=
  16  0 ≤ f.ppn_tight ∧ 0 ≤ f.lensing_band ∧ 0 ≤ f.gw_band
  17
  18/-- Default admissible bands (illustrative). -/
  19def falsifiers_default : Falsifiers :=
  20  { ppn_tight := (1/100000 : ℝ)
  21  , lensing_band := 1
  22  , gw_band := (1/1000000 : ℝ) }
  23
  24@[simp] theorem falsifiers_default_ok : falsifiers_ok falsifiers_default := by
  25  simp [falsifiers_ok, falsifiers_default]
  26  repeat' constructor <;> norm_num
  27
  28end ILG
  29end Relativity
  30end IndisputableMonolith

papers checked against this theorem

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