SpeciesEntry
The particle data record packages a string identifier with an observed mass, its experimental uncertainty, and a predicted mass value. Analysts comparing Recognition Science predictions to PDG measurements would cite this record when building test suites for quarks, leptons, or bosons. It is introduced by a direct structure definition with Repr derivation and no further content.
claimA record whose instances contain a string name, an observed real mass $m_ {obs}$, a real uncertainty $σ$, and a predicted real mass $m_{pred}$.
background
The PDG.Fits module assembles lists of particle measurements to test model predictions against experimental data. The uncertainty field records the standard deviation reported by experiment. The module imports sigma from decision theory, where it measures the gap between private preference and public vote, and from arithmetic functions as the sum-of-divisors, but employs the symbol locally for experimental error. Witness definitions such as baryonsWitness and bosonsWitness are built from instances of this record.
proof idea
The declaration is a structure definition that directly specifies the four fields and derives Repr for printing.
why it matters in Recognition Science
This record type is the common substrate for all fit-related definitions in the module, including the acceptable predicate that checks z-scores and chi-squared bounds, and concrete witnesses for baryons and bosons. It enables direct comparison of observed PDG masses against Recognition Science predictions derived from the phi-ladder. The structure closes the interface between experimental data and the theoretical mass formula.
scope and limits
- Does not compute z-scores or chi-squared values.
- Does not generate predicted masses from the phi-ladder.
- Does not store additional particle properties such as charge or spin.
- Does not validate consistency between observed and predicted masses.
- Does not specify physical units for the masses.
formal statement (Lean)
7structure SpeciesEntry where
8 name : String
9 mass_obs : ℝ
10 sigma : ℝ
11 mass_pred : ℝ
12 deriving Repr
13