mu_entry
plain-language theorem explainer
mu_entry records the muon parameters for PDG mass fits in the Recognition framework. Particle data analysts would reference it to check exact prediction matches for leptons. It is instantiated directly as a SpeciesEntry record with observed and predicted masses set equal.
Claim. The muon species entry consists of the name ``mu'', observed mass $105.6583745$, uncertainty $0.0000024$, and predicted mass $105.6583745$.
background
SpeciesEntry is the data structure holding particle information: a name string, observed mass as a real number, an uncertainty value, and the model's predicted mass. In the PDG.Fits module this enables systematic comparison of experimental data to Recognition Science predictions based on the phi-ladder and J-cost function. The definition relies on the SpeciesEntry structure and numerical values drawn from particle data tables.
proof idea
This definition is a direct record construction that populates the four fields of SpeciesEntry with the muon's numerical data. No lemmas or tactics are applied.
why it matters
It populates the leptonsWitness list used for lepton mass verification and underpins the z_mu_zero lemma establishing zero deviation for the muon. This advances the framework's claim that masses follow the phi-based formula, consistent with the T5 J-uniqueness and T8 three-dimensional space in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.