d_entry
plain-language theorem explainer
d_entry supplies the SpeciesEntry record for the down quark using observed mass 0.0047, uncertainty 0.0010 and predicted mass 0.0047. PDG mass-fit authors cite it when checking Recognition Science phi-ladder predictions against experimental quark data. The definition is a direct record literal with no computation or lemmas.
Claim. The down-quark entry is the record with name ``d'', observed mass $0.0047$, standard deviation $0.0010$, and predicted mass $0.0047$, where SpeciesEntry packages these four fields for each particle species.
background
Module PDG.Fits collects observed and predicted masses for Standard-Model particles to test Recognition Science mass predictions. SpeciesEntry is the structure with fields name : String, mass_obs : ℝ, sigma : ℝ (measurement uncertainty), mass_pred : ℝ. The sigma field here is the experimental uncertainty, distinct from the σ-charge defined in Decision.AbileneParadox and the divisor-sum function in NumberTheory.Primes.ArithmeticFunctions.
proof idea
Direct definition that constructs the SpeciesEntry record literal with the four supplied field values. No lemmas or tactics are invoked.
why it matters
The entry populates quarksWitness and is invoked by z_d_zero to establish vanishing defect for the d quark and by acceptable_quarks to verify the full quark list. It supplies concrete input data for testing the Recognition Science mass formula (yardstick times phi to the appropriate rung) against PDG values inside the PDG domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.