Z_entry
plain-language theorem explainer
Z_entry supplies the SpeciesEntry record for the Z boson using observed mass 91.1876 GeV, uncertainty 0.0021, and matching predicted mass. Researchers verifying boson mass predictions against PDG data within the Recognition Science phi-ladder would reference this entry when assembling fit lists. The definition proceeds by direct record construction of the SpeciesEntry structure.
Claim. The Z boson entry is the SpeciesEntry record with name ``Z'', observed mass $91.1876$, uncertainty $0.0021$, and predicted mass $91.1876$, where SpeciesEntry is the structure type with fields name : String, mass_obs : ℝ, sigma : ℝ, mass_pred : ℝ.
background
SpeciesEntry is the structure type holding particle data: a string name, observed real mass, real-valued uncertainty sigma, and real predicted mass. This definition lives in the PDG.Fits module, which assembles observed-versus-predicted entries for particle mass comparisons in the Recognition framework. Upstream results include the Z anchor map from Masses.Anchor that computes integer sector values for leptons and quarks, plus sigma definitions from arithmetic functions and decision theory that track charge gaps.
proof idea
The definition is a direct record literal that instantiates SpeciesEntry with the hardcoded Z boson values. No lemmas or tactics are invoked beyond the structure constructor.
why it matters
Z_entry populates the bosonsWitness list used by z_Z_zero to establish zero deviation for the Z mass. It supplies the PDG data slot in the mass fitting pipeline, aligning with the framework's mass formula and T5 J-uniqueness step. It closes the boson data provision without touching open questions on higher-rung predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.