Delta_0_entry
plain-language theorem explainer
Delta_0_entry supplies the PDG data record for the neutral Delta resonance with observed mass 1.232 GeV and matching prediction. Baryon spectroscopists checking Recognition Science mass fits against experiment cite this entry inside baryonsWitness and the acceptable_baryons lemma. The definition is a direct SpeciesEntry literal with no computation or lemmas.
Claim. The species entry for the neutral Delta resonance is the record with name ``Delta_0'', observed mass $1.232$, experimental uncertainty $0.005$, and predicted mass $1.232$.
background
SpeciesEntry is the structure that packages name, observed mass, uncertainty sigma, and predicted mass for each particle in the PDG.Fits module. The module assembles experimental PDG values for direct comparison with Recognition Science predictions on the phi-ladder. The sigma field here is the experimental uncertainty; it is unrelated to the sigma-charge defined in Decision.AbileneParadox or the divisor-sum function in NumberTheory.Primes.ArithmeticFunctions.
proof idea
Direct definition by structure literal; no tactics or upstream lemmas are invoked beyond the SpeciesEntry constructor.
why it matters
The entry populates baryonsWitness and is enumerated inside acceptable_baryons to verify all listed baryons meet the zero-defect criterion. It directly supports the z_D0_zero lemma. Within the Recognition framework it anchors the empirical 1.232 GeV mass for Delta_0 against the T5 J-uniqueness and mass-formula prediction, closing one link in the PDG-to-phi-ladder comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.