baryonsWitness
plain-language theorem explainer
BaryonsWitness assembles six SpeciesEntry records for the proton, neutron, and four Delta resonances, each pairing PDG-observed masses with Recognition Science predictions. Particle physicists validating the phi-ladder mass formula against experimental data cite this list when building the full defaultDataset for chi-squared tests. The definition is a direct enumeration of the six precomputed entry constants with no further computation.
Claim. Let baryonsWitness be the list of SpeciesEntry records $[p, n, Delta^{++}, Delta^{+}, Delta^{0}, Delta^{-}]$, where each record holds the particle name, observed mass $m_{obs}$, uncertainty $sigma$, and predicted mass $m_{pred}$ from the Recognition Science model.
background
In the PDG.Fits module, particle data is organized through the SpeciesEntry structure, which records for each species its name, observed mass, experimental uncertainty, and the mass predicted by the Recognition Science model. The six constituent entries are defined separately: proton and neutron carry precise PDG values near 0.938 and 0.940 GeV, while the four Delta states share a common observed mass of 1.232 GeV with 5 MeV uncertainty and identical predicted values. This list aggregates them for downstream chi-squared comparisons that test the zero-defect prediction for these baryons.
proof idea
The definition directly constructs the list by referencing the six precomputed SpeciesEntry constants for the proton, neutron, and Delta resonances. No tactic or reduction is applied; it is a literal list expression.
why it matters
This definition supplies the baryon component of defaultDataset, which is then used to prove that chi2_baryons_zero holds and that acceptable_baryons is satisfied. It supports validation that Recognition Science mass predictions match PDG data for these particles within uncertainties, closing the loop on the phi-ladder mass formula for baryons. It touches the T5 J-uniqueness and mass formula landmarks by providing concrete test cases for the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.