Delta_0_entry
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the mass value from the phi-ladder or any Recognition formula.
- Does not encode spin, isospin, or other quantum numbers.
- Does not cover leptons or non-baryon resonances.
Lean usage
have h : Delta_0_entry.mass_obs = 1.232 := by simp [Delta_0_entry]formal statement (Lean)
123@[simp] def Delta_0_entry : SpeciesEntry := { name := "Delta_0", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }