defaultDataset
plain-language theorem explainer
defaultDataset assembles the standard PDG lists of leptons, quarks, bosons, and baryons into one Dataset record. Particle physicists testing Recognition Science mass ladders against experiment would cite this as the fixed baseline input. The definition is a direct record construction from four precomputed witness lists.
Claim. The default dataset is the structure whose lepton field is the list of electron, muon and tau entries, whose quark field is the list of the six quark entries, whose boson field is the list of W, Z and Higgs entries, and whose baryon field is the list of proton, neutron and Delta entries.
background
In the PDG.Fits module a Dataset is the structure holding four lists of SpeciesEntry, one each for leptons, quarks, bosons and baryons. The four witness definitions supply the concrete PDG particles: leptonsWitness contains the three charged leptons, quarksWitness the six quarks, bosonsWitness the three gauge and Higgs bosons, and baryonsWitness the proton, neutron and four Delta states. These lists serve as the canonical experimental input for all subsequent acceptability and chi-squared checks in the module.
proof idea
The definition is a one-line record constructor that inserts the four witness lists leptonsWitness, quarksWitness, bosonsWitness and baryonsWitness directly into the Dataset fields.
why it matters
This definition supplies the concrete input to the lemma acceptable_all_default_zero, which confirms that the PDG baseline satisfies the zero-threshold acceptability condition for every species. It is also returned by the placeholder loadDatasetFromJson. Within the Recognition Science framework it anchors the PDG data layer used to confront the phi-ladder mass formula and J-cost predictions with measured particle properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.