Measurement
plain-language theorem explainer
A minimal experimental datum: a named observable with central value and one-sigma uncertainty. Used throughout the preregistered test harness so predictions can be compared to frozen measurement records without importing prediction modules into data modules. Pure structure definition; no proof content.
Claim. A measurement record is a triple $(n, c, \sigma)$ where $n$ is a string label, $c \in \mathbb{R}$ is the reported central value, and $\sigma \in \mathbb{R}$ is the one-sigma uncertainty.
background
The Preregistered Core module implements a structural separation: prediction modules must not import measurement modules; measurement modules hold pure data; test modules import both. The design goal is to enforce “formula frozen before measurement” inside the Lean build graph, not to prove historical preregistration.
This Measurement is the lightweight verification-side record: name, central value, and sigma. It is distinct from the richer RS-native measurement type (value, optional time window, protocol, optional uncertainty, notes) and from the quantum nonlocality measurement (axis, outcome, time). Sibling structures in the same module include interval and point predictions, plus containment and within-sigma predicates used when tests compare frozen predictions to these records.
proof idea
No proof. The declaration is a three-field structure (string name, real central value, real sigma) with the default generated constructor and projections. Downstream lemmas pattern-match on these fields or pass instances into comparison predicates such as interval containment and within-sigma checks.
why it matters
This type is the common currency for preregistered empirical checks across the monolith. Downstream consumers include alpha-genesis measurement verdicts (e.g. the certified $0.0007$ overshoot exceeding $30000\sigma$ against CODATA uncertainty), K-gate measurement packs for display invariance under units equivalence, W-mass CDF/ATLAS and SM-prediction records in the cosmology anomaly structure, and foundation-level measurement protocols (coupled vs uncoupled).
In Recognition Science terms it supports auditable comparison of derived constants (tau tick positivity, display ratios, alpha band claims) against external data without contaminating the prediction graph. It does not itself encode the forcing chain (T0–T8), RCL, or mass ladder; it only holds the numbers those claims are tested against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.