IndisputableMonolith.Verification.Preregistered.Hubble.Prediction

   1import Mathlib
   2import IndisputableMonolith.Verification.Preregistered.Core
   3import IndisputableMonolith.Constants
   4import IndisputableMonolith.Constants.Alpha
   5
   6/-!
   7# Preregistered Predictions: Hubble ratio and Ω_Λ
   8
   9This file intentionally contains **no observational numbers**.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Verification
  14namespace Preregistered
  15namespace Hubble
  16
  17open IndisputableMonolith.Constants
  18
  19noncomputable def hubble_ratio : PointPrediction :=
  20  { name := "H_late/H_early"
  21  , val := (13 : ℝ) / 12 }
  22
  23noncomputable def omega_lambda : PointPrediction :=
  24  { name := "Omega_L"
  25  , val := (11 : ℝ) / 16 - alpha / Real.pi }
  26
  27end Hubble
  28end Preregistered
  29end Verification
  30end IndisputableMonolith
  31