Measurement
plain-language theorem explainer
The Measurement structure supplies a minimal record holding a string identifier, a real central value, and an associated real uncertainty. Import routines and modules that consume electroweak or cosmological data cite this record to ingest hardcoded experimental points. The declaration is a plain structure with three fields and carries no proof obligations.
Claim. A measurement record consists of a string identifier together with a real number for the observed value and a real number for the reported uncertainty: $name : String$, $value, error : ℝ$.
background
The Data.Import module supplies experimental measurements for use throughout the Recognition Science library. The structure Measurement is defined here as a record with three fields. It is distinct from the Measurement structures appearing in Measurement.RSNative.Core (which adds protocol and window) and Quantum.NonlocalityNoSignaling (which adds axis and outcome).
proof idea
The declaration is a structure definition that introduces the three fields directly. No tactics or lemmas are applied; the body is empty as required for a structure.
why it matters
This record is consumed by import_measurements to populate lists containing the inverse fine-structure constant near 137.036, sin²θ_W, and α_s. Those lists support theorems on unit equivalence in KDisplay, W-mass anomaly comparisons in Cosmology, and cost models in Ethics. It therefore supplies the empirical anchor for checking Recognition Science predictions against data in the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.