Verification Preregistered Core

Preregistered testing

Verification preregistered core is a set of definitions in the framework's machine-checked library of formal theorems. Its purpose is to enforce a simple discipline: write the prediction formula before you look at the measurement. The library does this by separating the two into distinct modules. Prediction formulas live in modules that never import measurement modules. Measurements live in their own modules as pure data. A test module imports both and checks whether the prediction contains the measurement. This separation is structural, built into the dependency graph of the library itself, so a formula cannot quietly change after seeing the data.

The core defines three small structures. An interval prediction is a named range with a lower and upper bound. A point prediction is a named single value. A measurement is a named central value with a sigma, the experiment's resolution. The key test, interval containment, asks whether the measurement's central value lies strictly between the prediction's bounds. A second test, within_sigma, asks whether a point prediction lands within a chosen multiple of the measurement's sigma.

One definition does the real work: exposure. It is the width of the predicted interval divided by the measurement's sigma. This number answers a question the containment test alone cannot: could the test have failed at all? If the predicted interval is narrower than the measurement's resolution, exposure is below 1, and containment was a genuine test. If the interval is far wider than the resolution, exposure is large, and no plausible measurement could have contradicted the prediction. A separate definition, could_not_have_failed, states this directly: the interval is wider than k times the resolution.

The library records that this exposure idea was added after a sweep found the alpha inverse entry passing at an exposure of about 428571. That is a concrete case where a frozen interval was so wide that containment carried no information. The core does not prove that any particular prediction was historically preregistered. It enforces a clean, auditable separation inside the build graph, so a reader can check that the formula and the data never touched before the test ran.

structure IntervalPrediction where
  name : String
  lo : ℝ
  hi : ℝ

def within_sigma (p : PointPrediction) (m : Measurement) (k : ℝ := 1) : Prop :=
  |p.val - m.central| < k * m.sigma

/-- The width of the predicted interval measured in units of the experiment's
resolution. Below 1 the prediction is sharper than the measurement, so
containment was a real test. Far above 1 no measurement in the plausible range
could have contradicted it. -/
noncomputable def exposure (p : IntervalPrediction) (m : Measurement) : ℝ :=
  (p.hi - p.lo) / m.sigma

/-- The interval is wider than `k` times what the measurement can resolve. When
this holds for large `k`, `interval_contains` is not evidence: the measurement
would have landed inside for any central value in a range far exceeding its own
error bar. -/
def could_not_have_failed (p : IntervalPrediction) (m : Measurement) (k : ℝ) : Prop :=
  k * m.sigma < p.hi - p.lo

What this page does not claim

This module proves that any prediction was historically preregistered before its measurement. A wide interval that contains the measurement is treated as confirmation. The core defines what counts as a passing test beyond the structural separation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Preregistered/Core.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: