pionDecayConstant_MeV
plain-language theorem explainer
Pion decay constant is supplied as the numerical value 92.2 MeV. Researchers deriving pion masses via the GMOR relation in Recognition Science would reference this constant to verify order-of-magnitude consistency with observed values. The definition consists of a direct assignment without any reduction steps or lemmas.
Claim. The pion decay constant is defined as $f_π = 92.2$ MeV.
background
In the Pion Masses Derivation module, pions are treated as quark-antiquark bound states whose masses follow from chiral symmetry breaking and the Gell-Mann–Oakes–Renner (GMOR) relation $m_π² ∝ (m_u + m_d) × ⟨q̄q⟩. The module imports the Quark inductive type from CubeFaceUniversality, which enumerates the six quark flavors. The pion decay constant enters the GMOR formula as the normalization factor for the condensate.
proof idea
The declaration is a direct numerical definition that assigns the value 92.2 without invoking any lemmas or tactics.
why it matters
This constant supplies the normalization for the GMOR prediction defined downstream in gmorPrediction, which computes $2 × m_q × ⟨q̄q⟩ / f_π². It supports the theorem gmor_reasonable that confirms the prediction lies between 100 and 100000. Within the Recognition Science framework the value anchors the chiral condensate scale in the pion mass derivation (P-013), consistent with the φ-ladder placement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.