Delta_p_entry
plain-language theorem explainer
Delta_p_entry supplies the PDG data record for the Delta^+ resonance, fixing observed mass at 1.232, uncertainty at 0.005, and predicted mass at 1.232. Analysts assembling baryon mass fits cite this record when populating the witness list for acceptability checks. The definition is a direct record constructor for the SpeciesEntry structure.
Claim. Define the species entry for the Delta^+ resonance by the record with name ``Delta_p'', observed mass $1.232$, uncertainty $0.005$, and predicted mass $1.232$.
background
The PDG.Fits module assembles experimental particle data into standardized records to support mass predictions within the Recognition Science framework. SpeciesEntry is the structure type that packages a particle name, its observed mass, the associated uncertainty sigma, and a predicted mass value. This definition supplies the concrete data point for the Delta_p resonance, which is collected alongside the proton, neutron, and other Delta states in the baryonsWitness list.
proof idea
The definition is a one-line record literal that directly instantiates the SpeciesEntry constructor with the supplied numerical values.
why it matters
Delta_p_entry is included in baryonsWitness and thereby participates in the acceptable_baryons lemma, which verifies that the full baryon list satisfies the acceptable predicate at zero chi-squared. It supplies one experimental anchor for aligning PDG masses with the phi-ladder predictions of Recognition Science. The entry closes a data point in the baryon-sector verification chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.