IndisputableMonolith.Verification.Preregistered.Core

   1import Mathlib
   2
   3/-!
   4# Preregistered Test Harness (Core)
   5
   6Design goal: enforce “formula frozen before measurement” structurally.
   7
   8- **Predictions** live in modules that do **not** import measurement modules.
   9- **Measurements** live in separate modules (pure data).
  10- **Tests** import both.
  11
  12This doesn’t prove historical preregistration, but it enforces a clean, auditable
  13separation inside the Lean build graph.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Verification
  18namespace Preregistered
  19
  20structure IntervalPrediction where
  21  name : String
  22  lo : ℝ
  23  hi : ℝ
  24
  25structure PointPrediction where
  26  name : String
  27  val : ℝ
  28
  29structure Measurement where
  30  name : String
  31  central : ℝ
  32  sigma : ℝ
  33
  34def interval_contains (p : IntervalPrediction) (m : Measurement) : Prop :=
  35  p.lo < m.central ∧ m.central < p.hi
  36
  37def within_sigma (p : PointPrediction) (m : Measurement) (k : ℝ := 1) : Prop :=
  38  |p.val - m.central| < k * m.sigma
  39
  40end Preregistered
  41end Verification
  42end IndisputableMonolith
  43