pionIsospin
plain-language theorem explainer
The declaration assigns the pion isospin quantum number the value 1, matching the triplet representation of the three charge states under SU(2). Hadron physicists or chiral effective field theorists would cite this constant when applying the GMOR relation to extract quark mass differences from observed pion masses. The assignment is a direct constant definition with an attached comment on the pseudoscalar character.
Claim. The isospin quantum number of the pion is defined as $I = 1$.
background
The Pion Masses module derives the lightest meson masses from Recognition Science via quark-antiquark binding on the phi-ladder and the GMOR relation $m_π² ∝ (m_u + m_d) ⟨q̄q⟩. Pions occupy a specific rung that yields predicted masses near 139.6 MeV (charged) and 135.0 MeV (neutral), with the ratio to the electron mass near φ¹²/2. The supplied definition supplies the integer isospin needed for isospin-symmetric treatments inside that derivation.
proof idea
The definition is a direct constant assignment of the natural number 1. The accompanying comment records the pseudoscalar assignment J^P = 0^-. No lemmas or tactics are invoked.
why it matters
The definition supplies the isospin value required by the pion mass formulas and GMOR-based predictions in the module. It sits at the base of the P-013 derivation chain and is consistent with the phi-ladder placement and chiral symmetry breaking steps described in the module documentation. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.