pionChargedMass_MeV
plain-language theorem explainer
The definition supplies the PDG 2024 experimental value of the charged pion mass as 139.57039 MeV. Kaon-pion ratio theorems and GMO relation checks in the same module cite this constant directly as the numerical base for all subsequent mass comparisons. The declaration is a bare constant definition with no lemmas or reduction steps.
Claim. The charged pion mass is the constant $m_{π^±} = 139.57039$ MeV taken from PDG 2024 data.
background
The PionMasses module derives meson masses from Recognition Science by placing pions on the φ-ladder after quark-antiquark binding and explicit chiral symmetry breaking. The GMOR relation connects the squared pion mass to the product of light quark masses and the chiral condensate, while the φ-ladder fixes the absolute scale once the rung is chosen. The module imports Constants and PhiForcing to obtain the numerical φ value and the eight-tick octave structure that sets the mass spacing.
proof idea
Direct constant definition; no lemmas or tactics are applied.
why it matters
This value anchors every downstream mass-ratio theorem, including kaonPionRatio, kaon_pion_ratio_approx, kaon_pion_near_phi_sq_plus_1, and gmo_relation_approximate. It realizes the predicted π⁺ mass ≈ 139.6 MeV on the φ-ladder rung and supplies the base for the m_π/m_e ≈ 273 relation that matches φ^12/2. The constant therefore closes the numerical link between the Recognition Science mass formula and the observed meson spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.