Delta_pp_entry
plain-language theorem explainer
Delta_pp_entry supplies the SpeciesEntry record for the Delta++ baryon resonance, recording observed mass 1.232 GeV, uncertainty 0.005 GeV, and identical predicted mass. PDG mass-fitting work in Recognition Science cites this entry when constructing the baryon witness list for acceptability and zero-deviation checks. The definition is a direct record literal with no computation or lemma application.
Claim. The species entry for the resonance is the record with name ``Delta_pp'', observed mass $1.232$, uncertainty $0.005$, and predicted mass $1.232$.
background
The PDG.Fits module assembles particle data via the SpeciesEntry structure, a record holding a name string, observed mass, experimental uncertainty sigma, and predicted mass. This structure supports lists for baryons and leptons that are checked against Recognition Science mass predictions from the phi-ladder. The module imports Mathlib and references sigma from AbileneParadox (agent report gap) and from arithmetic functions (divisor sum), but here sigma is the uncertainty field. Local setting is verification of PDG fits for zero chi-squared and z-values.
proof idea
The declaration is a direct definition that constructs the SpeciesEntry record literal with the four fields for the Delta++ resonance. No lemmas or tactics are applied; it is a one-line record initialization.
why it matters
Delta_pp_entry populates the baryonsWitness list, which feeds acceptable_baryons and z_Dpp_zero. It supplies one slot in the PDG baryon fits, aligning the observed Delta++ mass with the Recognition Science mass formula yardstick * phi^(rung - 8 + gap(Z)) and the T5 J-uniqueness fixed point. This supports closure of the eight-tick octave checks for the Delta resonances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.