Dataset
plain-language theorem explainer
Dataset groups particle data into four lists of species entries covering leptons, quarks, bosons, and baryons for use in Recognition Science fits. Implementers of PDG validation or empiricalStatus checks cite this structure when supplying observed masses, uncertainties, and model predictions. The declaration is a direct structure definition with four list fields and no proof content.
Claim. A dataset consists of four lists of species entries, one each for leptons, quarks, bosons, and baryons. Each species entry records a particle name, an observed real-valued mass, an experimental uncertainty, and a model-predicted real-valued mass.
background
SpeciesEntry is the atomic record holding a particle name as a string together with its observed mass, measurement uncertainty, and predicted mass, all as real numbers. Dataset collects these records into four category lists so that aggregate predicates can test fit quality across particle sectors. The PDG.Fits module supplies this data carrier to connect empirical measurements with the Recognition mass formulas.
proof idea
The declaration is a structure definition that introduces the four list fields directly. No lemmas, tactics, or reductions are applied.
why it matters
Dataset supplies the input type for acceptable_all, defaultDataset, and loadDatasetFromJson, which feed the empiricalStatus classification in OptionAFalsifierRegistry. It marks PDG content as carrying an empirical hypothesis and closes the data interface for testing phi-ladder mass predictions against observations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.