`IsConsistentWithRS`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.HubbleTensionBound on GitHub at line 56.

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

  53
  54/-- A measurement is consistent with the RS prediction iff it sits in
  55the predicted band. -/
  56def IsConsistentWithRS (h0_ratio : ℝ) : Prop :=
  57  hubbleRatioLower < h0_ratio ∧ h0_ratio < hubbleRatioUpper
  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

papers checked against this theorem

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