`IndisputableMonolith.Verification.Preregistered.AlphaInv.Test`

IndisputableMonolith/Verification/Preregistered/AlphaInv/Test.lean · 26 lines · 1 declarations

Explainer status: ready · generated 2026-08-13 16:34:00.179922+00:00

   1import Mathlib
   2import IndisputableMonolith.Verification.Preregistered.Core
   3import IndisputableMonolith.Verification.Preregistered.AlphaInv.Prediction
   4import IndisputableMonolith.Verification.Preregistered.AlphaInv.Measurement_CODATA2022
   5
   6/-!
   7# Test: α⁻¹ RS interval contains CODATA 2022
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Verification
  12namespace Preregistered
  13namespace AlphaInv
  14
  15theorem passes_CODATA2022 :
  16    interval_contains prediction measurement_CODATA2022 := by
  17  -- This test is intentionally “dumb”: it checks the declared interval contains the
  18  -- declared measurement. Tightening the interval is handled in AlphaBounds.
  19  unfold interval_contains prediction measurement_CODATA2022
  20  norm_num
  21
  22end AlphaInv
  23end Preregistered
  24end Verification
  25end IndisputableMonolith
  26

source mirrored from github.com/jonwashburn/shape-of-logic