z_mu_zero
plain-language theorem explainer
The muon zero-cost lemma asserts that the recognition cost evaluates to zero for the muon species entry. Particle data group fits within Recognition Science would cite this when confirming exact agreement between predicted and observed muon mass. The proof is a one-line simplification using the cost definition and division rewriting.
Claim. Let $z$ be the recognition cost function. For the muon entry with observed mass equal to predicted mass, $z = 0$.
background
Species entries are records holding a name, observed mass, uncertainty sigma, and predicted mass. The muon entry sets observed and predicted masses equal at 1056583745 / 10000000000.0 with sigma 24 / 10000000000.0. The z function measures normalized deviation, vanishing on exact mass matches. This lemma rests on the mu_entry definition and supports zero-deviation results for the lepton set.
proof idea
This is a one-line wrapper proof. It applies the simp tactic with the z definition and the div_eq_mul_inv identity to reduce the goal to a trivial equality.
why it matters
The result feeds chi2_leptons_zero, which establishes vanishing chi-squared for the lepton witness, and acceptable_leptons, which confirms fit acceptability. It verifies the exact PDG match for the muon under the Recognition Science mass formula. It supports alignment of the phi-ladder predictions with lepton data at experimental precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.