n_entry
plain-language theorem explainer
n_entry supplies the neutron data point for PDG mass fits in Recognition Science. Particle data analysts checking baryon predictions on the phi-ladder would cite this entry. The definition constructs the SpeciesEntry record directly with observed and predicted masses set equal.
Claim. Define the neutron entry as the SpeciesEntry record with name ``n'', observed mass $0.9395654133$, uncertainty $10^{-6}$, and predicted mass $0.9395654133$.
background
The PDG.Fits module assembles experimental mass data from the Particle Data Group for comparison against Recognition Science predictions. SpeciesEntry is the record type holding a string name, observed mass, measurement uncertainty sigma, and model-predicted mass for each particle. This neutron entry joins proton and Delta entries inside baryonsWitness to enable zero-defect verification via the z function.
proof idea
Direct definition by record literal that assigns the PDG values for the neutron.
why it matters
It populates baryonsWitness and feeds the lemmas acceptable_baryons and z_n_zero that confirm zero chi-squared contribution for the neutron. This integrates PDG data into the framework's validation of J-uniqueness and the phi fixed point for baryon masses on the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.