IndisputableMonolith.Verification.Preregistered.AlphaInv.Prediction

   1import Mathlib
   2import IndisputableMonolith.Verification.Preregistered.Core
   3import IndisputableMonolith.Constants
   4import IndisputableMonolith.Constants.Alpha
   5import IndisputableMonolith.Numerics.Interval.AlphaBounds
   6
   7/-!
   8# Preregistered Prediction: α⁻¹ (inverse fine-structure constant)
   9
  10This file intentionally contains **no experimental values**.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Verification
  15namespace Preregistered
  16namespace AlphaInv
  17
  18open IndisputableMonolith.Constants
  19open IndisputableMonolith.Numerics
  20
  21def prediction : IntervalPrediction :=
  22  { name := "alphaInv"
  23  , lo := 137.030
  24  , hi := 137.039 }
  25
  26theorem lo_verified : prediction.lo < alphaInv := by
  27  simpa [prediction, IntervalPrediction.lo] using (alphaInv_gt : (137.030 : ℝ) < alphaInv)
  28
  29theorem hi_verified : alphaInv < prediction.hi := by
  30  simpa [prediction, IntervalPrediction.hi] using (alphaInv_lt : alphaInv < (137.039 : ℝ))
  31
  32end AlphaInv
  33end Preregistered
  34end Verification
  35end IndisputableMonolith
  36