`IndisputableMonolith.Predictions`

IndisputableMonolith/Predictions.lean · 21 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Predictions.Row
   2import IndisputableMonolith.Predictions.ExperimentalAnchors
   3import IndisputableMonolith.Predictions.Registry
   4import IndisputableMonolith.Predictions.Comparison
   5import IndisputableMonolith.Predictions.Certificate
   6
   7/-!
   8# RS Predictions Pipeline — Aggregator
   9
  10Imports the full numerical falsification pipeline:
  11
  12- `Row`: `PredictionRow` type, `containment`, `ppm_deviation`, `sigma_tension`
  13- `ExperimentalAnchors`: quarantined CODATA 2022 / PDG 2024 values
  14- `Registry`: master list of 20 derived quantities (Tiers A–D)
  15- `Comparison`: machine-verified containment proofs
  16- `Certificate`: `RSPredictions2026Cert` master certificate
  17
  18The LaTeX/JSON export executable is separate (`Predictions.Export`)
  19and registered as `lean_exe predictions_export` in the lakefile.
  20-/
  21

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