p_entry
p_entry defines the proton as a SpeciesEntry record in the PDG fits module, setting observed and predicted masses both to 0.9382720813 with uncertainty 1e-6. Baryon fit constructions such as baryonsWitness and lemmas like acceptable_baryons and z_p_zero reference this entry when building witness lists for zero-deviation checks. The definition is a direct record literal with no computation or lemma applications.
claimThe proton entry is the SpeciesEntry record with name ``p'', observed mass $0.9382720813$, uncertainty $10^{-6}$, and predicted mass $0.9382720813$.
background
The PDG.Fits module encodes Particle Data Group measurements as SpeciesEntry records to compare against Recognition Science mass predictions. SpeciesEntry is a structure with fields name (String), mass_obs (ℝ), sigma (ℝ), and mass_pred (ℝ). This supplies concrete data points for deviation functions such as z and chi2 in the module.
proof idea
This is a direct definition that constructs the SpeciesEntry record using the supplied numerical constants. No lemmas or tactics are applied; it functions as a constant data value for downstream list constructions and simplifications.
why it matters in Recognition Science
p_entry populates the baryonsWitness list, which is used by acceptable_baryons to verify fit acceptance across baryons and by z_p_zero to establish zero deviation for the proton. It anchors PDG data integration in the Recognition Science framework, supporting tests of the phi-ladder mass formula against experimental hadron masses.
scope and limits
- Does not derive the predicted mass from the phi-ladder or Recognition Science equations.
- Does not compute deviations, chi-squared values, or fit statistics.
- Does not include other baryons, leptons, or additional species.
- Does not specify physical units or external data validation.
formal statement (Lean)
119@[simp] def p_entry : SpeciesEntry := { name := "p", mass_obs := 0.9382720813, sigma := 1e-6, mass_pred := 0.9382720813 }