import_measurements
plain-language theorem explainer
A fixed list of six experimental measurements supplies benchmark values for the inverse fine-structure constant, weak mixing angle, strong coupling, and lepton g-2 anomalies. Modelers checking Recognition Science predictions against data cite this collection when testing the phi-ladder against PDG entries. The definition simply enumerates the records with their reported central values and uncertainties.
Claim. Let $M$ be the list containing the records (``AlphaInvPrediction'', $137.035999084$, $8.4times10^{-8}$), (``Sin2ThetaW_at_MZ'', $0.23121$, $4times10^{-5}$), (``AlphaS_at_MZ'', $0.1179$, $9times10^{-4}$), (``ElectronG2'', $0.00115965218073$, $2.8times10^{-13}$), (``MuonG2'', $0.00116592062$, $4.1times10^{-10}$), and (``MW_over_MZ'', $0.88153$, $1.8times10^{-4}$).
background
The Measurement structure is a record with three fields: a string name, a real central value, and a real uncertainty. The Data.Import module provides this static collection because JSON parsing is blocked by the current Mathlib version. Upstream Measurement definitions in RSNative.Core and Quantum.NonlocalityNoSignaling add protocol and window fields, but the present list uses the minimal three-field form for direct numeric comparison.
proof idea
The definition is realized by a direct list literal that constructs six Measurement instances from the supplied numeric literals.
why it matters
This list anchors the verification definitions verify_ns in Cosmology.Predictions and mass_ladder_matches_pdg in Masses.Basic. It supplies the empirical targets against which the Recognition Science constants (phi-ladder, alpha band near 137.036) are tested. The hardcoded status marks a temporary scaffold pending implementation of external data ingestion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.