pionSpin
plain-language theorem explainer
Assigns the pion spin quantum number the value zero. Hadron physicists reference the constant when evaluating selection rules in pion decays or constructing effective Lagrangians for strong-interaction processes. The entry is a bare constant definition requiring no supporting lemmas or reductions.
Claim. The pion has spin quantum number $s = 0$.
background
The PionMasses module derives charged and neutral pion masses from Recognition Science. Pions are treated as quark-antiquark bound states whose binding follows phi-ladder patterns, with nonzero masses arising from explicit chiral symmetry breaking via the GMOR relation $m_π^2 ∝ (m_u + m_d) ⟨q̄q⟩$. The module also records the predicted ratio $m_π / m_e ≈ φ^{12}/2$ and the electromagnetic splitting between charged and neutral states.
proof idea
Direct constant assignment of the natural number 0 with no lemmas or tactics applied.
why it matters
Supplies the angular-momentum input required by all sibling mass and ratio definitions in the module. It is consistent with the pseudoscalar classification of the pion and with the phi-ladder placement of mesons under the Recognition Science forcing chain. No downstream theorems are recorded, so the definition functions as a primitive constant for the pion sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.