u_entry
plain-language theorem explainer
u_entry records the PDG data for the up quark as a SpeciesEntry structure, supplying observed mass 0.0022 with uncertainty 0.0005 and matching predicted mass. Researchers fitting quark masses on the Recognition Science phi-ladder would cite this constant data point when verifying the mass formula against experiment. The definition is a direct record construction with no computation or lemmas applied.
Claim. The up-quark entry is the record with name $u$, observed mass $0.0022$, uncertainty $0.0005$, and predicted mass $0.0022$.
background
SpeciesEntry is the structure holding particle identification and mass data: a name string together with observed mass, its uncertainty sigma, and the predicted mass from the model. In the PDG.Fits module this supplies concrete numerical inputs for the six quark species. The definition draws on the structure declaration in the same module and is independent of the unrelated sigma functions imported from Decision and NumberTheory modules.
proof idea
The definition is a direct record construction that populates the four fields of SpeciesEntry with the supplied constants for the up quark. No lemmas are applied.
why it matters
This entry populates the quarksWitness list and is checked by acceptable_quarks and z_u_zero. It supplies the experimental anchor for the up-quark rung on the phi-ladder mass formula in the PDG fits. Within Recognition Science it tests the mass prediction against PDG values, closing one data point in the quark sector verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.