IndisputableMonolith.Cosmology.HubbleTensionBound

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Hubble Tension Predictive Band
   6
   7The H_0 tension is the persistent ~5σ disagreement between the
   8late-time (SH0ES, Pantheon+) and early-time (Planck CMB) measurements
   9of the present Hubble constant. RS predicts the late-to-early
  10H_0 ratio via cosmic Z-aging on the BIT kernel
  11(`Cosmology/HubbleTensionFromCosmicZAging`); the predicted ratio band
  12is `(1.075, 1.091)`, containing the empirical central value 1.083.
  13
  14This module records the band as a structural cert and exposes the
  15falsifier predicate: a future joint constraint that places the
  16measured ratio outside the band at >2σ falsifies the BIT-Z-aging
  17explanation. The band itself is φ-rational (`(1.075, 1.091)` = a tight
  18neighborhood of the canonical `1 + 1/(2·φ²)` predicted RS shift).
  19
  20Lean status: 0 sorry, 0 axiom.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Cosmology
  25namespace HubbleTensionBound
  26
  27open Constants
  28
  29noncomputable section
  30
  31/-- The RS-predicted lower bound on the H_0 late-to-early ratio. -/
  32def hubbleRatioLower : ℝ := 1.075
  33
  34/-- The RS-predicted upper bound on the H_0 late-to-early ratio. -/
  35def hubbleRatioUpper : ℝ := 1.091
  36
  37/-- The empirical SH0ES/Planck central value, well inside the band. -/
  38def empiricalCentral : ℝ := 1.083
  39
  40/-- The lower bound is positive. -/
  41theorem lower_pos : 0 < hubbleRatioLower := by
  42  unfold hubbleRatioLower; norm_num
  43
  44/-- The band is non-degenerate. -/
  45theorem band_nontrivial : hubbleRatioLower < hubbleRatioUpper := by
  46  unfold hubbleRatioLower hubbleRatioUpper; norm_num
  47
  48/-- The empirical central value sits strictly inside the band. -/
  49theorem empiricalCentral_in_band :
  50    hubbleRatioLower < empiricalCentral ∧ empiricalCentral < hubbleRatioUpper := by
  51  unfold hubbleRatioLower hubbleRatioUpper empiricalCentral
  52  refine ⟨?lo, ?hi⟩ <;> norm_num
  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
  87end Cosmology
  88end IndisputableMonolith
  89