leptonsWitness
plain-language theorem explainer
leptonsWitness assembles the three charged lepton entries into a list for PDG-style fitting. Analysts testing Recognition Science mass predictions against experimental data cite this list when checking zero-chi-squared conditions for leptons. The definition is a direct enumeration of the precomputed electron, muon, and tau entries.
Claim. The lepton witness list is the list containing the electron entry, the muon entry, and the tau entry, where each entry records a particle name, observed mass, experimental uncertainty, and model-predicted mass.
background
The SpeciesEntry structure records for each particle its name, observed mass, experimental uncertainty sigma, and the mass predicted by the Recognition Science model. Upstream definitions supply the concrete values: the electron entry with matching observed and predicted mass, the muon entry, and the tau entry. This definition lives in the PDG.Fits module that prepares the default dataset for chi-squared comparisons between model predictions and PDG measurements.
proof idea
This is a one-line definition that constructs the list by enumerating the three pre-defined lepton entries.
why it matters
The list is consumed by the lemmas chi2_leptons_zero and acceptable_leptons, which establish that the Recognition Science predictions match observed lepton masses within experimental error. It forms the lepton component of the defaultDataset used for broader particle fits. In the framework it supports verification of the mass formula on the phi-ladder for the charged leptons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.