Delta_m_entry
plain-language theorem explainer
Delta_m_entry records the PDG data point for the Delta(1232) resonance with observed mass 1.232 GeV, uncertainty 0.005, and matching predicted mass. Particle physicists assembling baryon spectra in the Recognition framework cite this entry inside the baryonsWitness list for zero-deviation checks. The definition is a direct record literal that populates the four fields of the SpeciesEntry structure.
Claim. The resonance entry is the record structure with name ``Delta_m'', observed mass $1.232$, uncertainty $0.005$, and predicted mass $1.232$.
background
The PDG.Fits module assembles observed and predicted masses for leptons and baryons to test Recognition Science mass predictions. SpeciesEntry is the record type carrying a string name, observed mass, experimental uncertainty sigma, and predicted mass. The sigma field stores the PDG error bar directly, distinct from the sum-of-divisors function or decision-theoretic sigma appearing in sibling modules.
proof idea
The definition is a one-line record literal that applies the SpeciesEntry constructor to the four supplied constants.
why it matters
Delta_m_entry completes the baryonsWitness list that feeds acceptable_baryons and the zero lemmas z_Dm_zero. It anchors the Delta resonance to the phi-ladder mass formula at the eight-tick octave, where predicted and observed values coincide within the stated uncertainty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.