s_entry
plain-language theorem explainer
s_entry supplies the data record for the strange quark in the PDG fits collection, fixing its observed mass at 0.096 with uncertainty 0.0050 and an identical predicted value. Quark-mass modelers testing the phi-ladder predictions against PDG data would cite this entry when assembling the six-quark witness list. The definition is a direct record literal with no further computation or lemmas applied.
Claim. The strange-quark entry is the record with name ``s'', observed mass $0.096$, uncertainty $0.0050$, and predicted mass $0.096$.
background
SpeciesEntry is the structure that packages a particle name together with its observed mass, the associated uncertainty sigma, and the model-predicted mass. In the PDG.Fits module these records are collected for leptons and quarks to compare Recognition Science mass predictions against experimental values. The sigma field here records the standard deviation of the observed mass; it is unrelated to the sigma-charge defined in the AbileneParadox module or the divisor-sum function from ArithmeticFunctions.
proof idea
One-line definition that constructs the SpeciesEntry record literal directly.
why it matters
The entry is referenced by quarksWitness to build the list of six quark records and is discharged inside acceptable_quarks and z_s_zero. It therefore participates in the verification that all quark predictions lie inside their PDG uncertainty bands, supporting the mass formula yardstick * phi^(rung-8+gap(Z)) on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.