u_entry
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the predicted mass from the Recognition mass formula.
- Does not cover leptons or other particle families.
- Does not perform any chi-squared computation.
- Does not assert agreement between observed and predicted values.
Lean usage
example : z u_entry = 0 := z_u_zeroformal statement (Lean)
60@[simp] def u_entry : SpeciesEntry := { name := "u", mass_obs := 0.0022, sigma := 0.0005, mass_pred := 0.0022 }