IndisputableMonolith.Relativity.ILG.Falsifiers

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Relativity
   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
  31