Pith. sign in
module module moderate

IndisputableMonolith.Verification.Preregistered.Core

show as:
view Lean formalization →

Shared Lean types and predicates for preregistered Recognition Science predictions versus lab data. Defines interval and point predictions, measurements with uncertainty, and checks that a datum lies in a predicted band or within n sigma. Every constant-test suite (inverse fine structure, strong coupling, Hubble) imports this core. Pure definitions and decidable predicates; no theorems.

claimThe module introduces an interval prediction $[\ell,u]$, a point prediction with stated uncertainty, a measurement $m\pm\sigma$, and the predicates that $m$ lies in $[\ell,u]$ and that $|m-p|\le n\sigma$ for a predicted central value $p$.

background

Recognition Science freezes numerical claims before confronting experiment. This core module is the shared vocabulary for that discipline: a prediction is recorded as either a closed real interval or a central value with an explicit error model, and a measurement is a central value with its reported uncertainty. No experimental numbers live here; pure data modules and pure prediction modules import these types separately so that updates to CODATA or PDG cannot silently rewrite the frozen claim.

Sibling definitions supply IntervalPrediction, PointPrediction, Measurement, together with the Boolean checks interval_contains and within_sigma. The surrounding verification domain uses them to keep the RS-native bands (for example the $\alpha^{-1}$ window near $137.03$–$137.04$) cleanly separated from the lab releases that will be compared against them.

proof idea

This is a definition module: it declares structures and decidable predicates only. There are no theorems and no proof obligations beyond the ordinary Lean type-checking of the field projections and the arithmetic comparisons inside the containment and sigma checks.

why it matters in Recognition Science

Every preregistered constant test in the monolith imports this core. Downstream modules include the $\alpha^{-1}$ CODATA 2022 measurement and its matching test ("RS interval contains CODATA 2022"), the $\alpha_s(M_Z)$ PDG measurement and its within-$1\sigma$ test, and the parallel Hubble 2022 measurement/prediction/test triple. By forcing predictions and measurements through a single pair of types, the framework keeps the RS forcing-chain outputs (T5 J-cost uniqueness, the $\phi$-ladder mass and coupling formulae, the quoted $\alpha^{-1}$ band) auditable against successive data releases without editing the claim side.

scope and limits

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (5)