`IsFalsifier`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.HubbleTensionBound
domain: Cosmology
line: 61 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.HubbleTensionBound on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  58
  59/-- A measurement is a falsifier iff it sits below the predicted band by
  60more than the band width (rough 2σ proxy). -/
  61def IsFalsifier (h0_ratio : ℝ) : Prop :=
  62  h0_ratio < hubbleRatioLower - (hubbleRatioUpper - hubbleRatioLower)
  63
  64/-- Consistency and falsification are mutually exclusive. -/
  65theorem consistency_excludes_falsification {h0 : ℝ} :
  66    ¬ (IsConsistentWithRS h0 ∧ IsFalsifier h0) := by
  67  rintro ⟨⟨h_lo, _⟩, h_excl⟩
  68  unfold IsFalsifier at h_excl
  69  unfold hubbleRatioLower hubbleRatioUpper at *
  70  linarith
  71
  72structure HubbleTensionCert where
  73  band_nontrivial : hubbleRatioLower < hubbleRatioUpper
  74  empirical_in_band :
  75    hubbleRatioLower < empiricalCentral ∧ empiricalCentral < hubbleRatioUpper
  76  consistency_excludes_falsification :
  77    ∀ {h0 : ℝ}, ¬ (IsConsistentWithRS h0 ∧ IsFalsifier h0)
  78
  79/-- Hubble-tension predictive-band certificate. -/
  80def hubbleTensionCert : HubbleTensionCert where
  81  band_nontrivial := band_nontrivial
  82  empirical_in_band := empiricalCentral_in_band
  83  consistency_excludes_falsification := consistency_excludes_falsification
  84
  85end
  86end HubbleTensionBound
  87end Cosmology
  88end IndisputableMonolith

papers checked against this theorem

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