Pith. sign in
module module moderate

IndisputableMonolith.Verification.Preregistered.Core

show as:
view Lean formalization →

Shared types and predicates for preregistered Recognition Science predictions versus experimental measurements. Supplies interval and point prediction records, measurement records, and containment or sigma-match checks. AlphaInv, AlphaS, and Hubble measurement, prediction, and test modules import this core so theory files stay free of lab values. Pure definitional module with no theorems.

claimThe module defines interval predictions $[\ell,u]$, point predictions $x\in\mathbb{R}$, measurement records $(v,\sigma)$, the predicate that $[\ell,u]$ contains a measured central value, and the predicate that a point lies within $k\sigma$ of a measurement.

background

Recognition Science preregisters numerical claims (inverse fine-structure band, strong coupling at $M_Z$, Hubble scale, and related constants) before any comparison to CODATA or PDG releases. Verification is organized so Prediction modules hold only theory-side numbers, Measurement modules hold only experimental central values and uncertainties, and Test modules combine the two.

This Core module is the shared vocabulary for that split. It introduces interval and point prediction structures, a measurement record, and the two standard scientific checks: whether a predicted interval contains the measured value, and whether a point prediction lies inside a stated multiple of the experimental sigma. Downstream files import only Mathlib plus this core.

proof idea

This is a definition module, no proofs. It declares data structures and decidable predicates (interval containment, within-$k\sigma$ match) that Test modules apply to concrete Prediction and Measurement values.

why it matters in Recognition Science

Feeds the entire preregistered verification suite under Verification.Preregistered: AlphaInv (CODATA 2022 $\alpha^{-1}$), AlphaS (PDG $\alpha_s(M_Z)$), and Hubble measurement, prediction, and test modules. Downstream docs stress pure data Measurement files ("update here when a future release arrives") and Prediction files that "intentionally contain no experimental values." The separation keeps the RS $\alpha^{-1}$ band and other forced constants auditable against lab updates without mixing theory and data. Supports the framework landmark that $\alpha^{-1}$ lies in $(137.030, 137.039)$ in RS-native units.

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)