z
plain-language theorem explainer
z standardizes the residual between a Recognition Science mass prediction and the PDG observed value for any particle species entry. PDG fit analysts and mass-ladder validators cite it when quantifying agreement on the phi-ladder. The definition is a direct one-line arithmetic expression on the four fields of SpeciesEntry.
Claim. For a species entry $e$ carrying observed mass $m_0$, uncertainty $s$, and model prediction $m_p$, define $z(e) = (m_p - m_0)/s$.
background
The PDG.Fits module encodes experimental particle data through the SpeciesEntry structure, whose fields are a name string, observed mass, experimental uncertainty sigma, and the mass predicted by the Recognition Science model. The local setting is therefore the comparison of phi-ladder mass formulas against PDG tables, with z supplying the normalized residual needed for chi-squared statistics. Upstream imports include the sigma-charge definition from Decision.AbileneParadox and the divisor-sum sigma from NumberTheory.Primes, but neither is used here; only the sigma field inside SpeciesEntry appears in the body.
proof idea
One-line definition that subtracts the observed mass from the predicted mass and divides by the sigma field of the supplied SpeciesEntry.
why it matters
z supplies the per-species residual that feeds the chi2 and acceptable predicates inside the same module, enabling the leptonsWitness and zero-residual statements for electrons, muons, and taus. It therefore closes the loop from the mass formula (yardstick times phi to a rung) to direct experimental comparison, supporting the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.