e_entry
plain-language theorem explainer
e_entry supplies the PDG data record for the electron with observed mass 0.51099895, uncertainty 10^{-9}, and predicted mass set equal to the observed value. Analysts fitting lepton masses to the Recognition phi-ladder cite this record to verify zero defect. The definition is a direct structure literal with no computation or derivation.
Claim. The electron species entry is the structure with name ``e'', observed mass $0.51099895$, uncertainty $10^{-9}$, and predicted mass $0.51099895$.
background
SpeciesEntry is the structure holding a particle name as string together with real-valued observed mass, uncertainty sigma, and predicted mass. The PDG.Fits module assembles such records for leptons to test numerical consistency with Recognition Science mass predictions. The local setting uses Mathlib reals and supplies concrete PDG values without invoking the upstream sigma definitions from AbileneParadox or arithmetic functions.
proof idea
The definition is a direct structure constructor application that supplies literal rational values for the electron's PDG data.
why it matters
This entry populates the leptonsWitness list and supports the lemma z_e_zero that establishes zero defect for the electron. It contributes to checking the Recognition mass formula against PDG data, aligning with the T5 J-uniqueness step and the phi-ladder construction. It closes a concrete data point in the PDG domain without addressing open questions on quark fits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.