loadDatasetFromJson
plain-language theorem explainer
This definition supplies a placeholder function that accepts a file path and returns an IO action yielding a Dataset of particle species lists. Code performing PDG fits or chi-squared checks would call it to initialize data. The body is a one-line wrapper that discards the path argument and returns the hardcoded defaultDataset via pure.
Claim. The function loadDatasetFromJson takes a file path of type System.FilePath and produces an IO action returning a Dataset, where Dataset is the structure whose fields are lists of SpeciesEntry for leptons, quarks, bosons, and baryons; the current implementation returns the default dataset.
background
In the PDG.Fits module the Dataset structure organizes empirical particle data into four parallel lists: leptons, quarks, bosons, and baryons, each holding SpeciesEntry records. The sibling defaultDataset supplies a concrete value built from category-specific witnesses such as leptonsWitness. The upstream System structure from BoltzmannDistribution defines a nonempty list of energy levels, providing the broader thermodynamic context in which these particle datasets are later used for distribution calculations.
proof idea
The definition is a one-line wrapper that applies the pure constructor directly to defaultDataset.
why it matters
This placeholder closes the data-loading interface inside the PDG.Fits module, allowing the rest of the fits machinery (chi-squared, acceptable checks, lepton witnesses) to compile and run against a fixed dataset. It supports the Recognition Science program by supplying the empirical inputs needed to test mass-ladder predictions and coupling constants against PDG values. The definition will be replaced once a concrete JSON parser is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.