muon_mass_MeV_pos
plain-language theorem explainer
The lemma confirms that the muon mass value imported from PDG 2024 is strictly positive. Researchers comparing Recognition Science cost derivations to particle data would cite it as a minimal sanity check on the external anchor. The proof reduces directly via the norm_num tactic applied to the numerical definition.
Claim. $0 < m_μ$ where $m_μ = 105.6583755$ MeV/$c^2$ is the muon mass from PDG 2024.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data entering Recognition Science. Its policy keeps the cost-first core (RCL derivations) free of external numbers while allowing downstream modules to import CODATA and PDG values under the external_anchor attribute. The upstream definition muon_mass_MeV sets the muon mass to the literal 105.6583755 MeV/c².
proof idea
One-line wrapper that applies the norm_num tactic to the definition of muon_mass_MeV, reducing the strict inequality to a direct numerical check on the positive literal.
why it matters
The result supplies a basic positivity guard for the muon mass external anchor, enabling safe use in comparisons between RS-native constants and experiment. It sits in the Constants.ExternalAnchors module whose purpose is mechanical separation of empirical data from the pure cost derivation. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.