module module moderate

`IndisputableMonolith.Physics.PionMasses`

Module collecting PDG pion masses, the RS phi-ladder rung for the pion, and predicted pion/electron mass ratios. Supplies the charged and neutral MeV/eV anchors used by meson mass derivations. Downstream kaon work imports these constants and the binary-gauge rung assignment. Mostly definitions and numerical comparisons, not a deep proof chain.

claimPDG charged and neutral pion masses $m_{\pi^\pm}$, $m_{\pi^0}$ (MeV and eV), the pion rung on the $\varphi$-ladder, the meson binary gauge, the RS-predicted pion mass in eV, and the ratios $m_\pi/m_e$ (PDG vs predicted), with lemmas that the charged mass is near $140\,\mathrm{MeV}$ and exceeds the neutral mass.

background

Recognition Science places particle masses on a discrete $\varphi$-ladder: mass equals a yardstick times $\varphi$ raised to a rung offset (primer: yardstick $\cdot \varphi^{rung-8+gap(Z)}$). The golden ratio $\varphi$ is forced by self-similarity of a discrete ledger with $J$-cost (PhiForcing). Constants supplies the RS time quantum $\tau_0=1$ tick and related unit conversions.

This module is the pion sector of that ladder. It records PDG 2024 charged and neutral pion masses in MeV and eV, assigns a pion rung and a meson binary gauge, and forms the predicted pion mass and the pion-to-electron mass ratio. Electron mass in eV is included so the ratio is self-contained.

The local setting is pure physics bookkeeping: numerical anchors and simple inequalities, not a new forcing step. KaonMasses later reuses the same pattern for strange mesons.

proof idea

Definition-heavy module. Masses and rungs are def/abbrev constants (PDG values and RS rung assignments). Predicted mass and ratios are arithmetic on those constants and $\varphi$ from PhiForcing/Constants. The two named lemmas are short numerical facts: charged pion mass lies near $140,\mathrm{MeV}$, and charged exceeds neutral. No multi-step tactic proofs or deep lemma chains.

why it matters in Recognition Science

Feeds IndisputableMonolith.Physics.KaonMasses, which derives $K^\pm$ and $K^0$ masses from the same RS meson mechanism (strange-quark content on the $\varphi$-ladder). Without fixed pion anchors and the shared meson binary gauge, the kaon sector has no calibrated baseline. Sits in the mass-formula layer of the framework (phi-ladder rungs), not in the T0–T8 forcing chain itself. Closes the lightest-meson numerical interface so heavier mesons can cite a common rung and ratio style.

scope and limits

Does not derive pion masses from first principles; PDG values are inputs.
Does not prove the general mass formula or force $\varphi$; that lives in PhiForcing and upstream mass theory.
Does not treat kaon, eta, or baryon masses; only pion anchors and ratios.
Does not address decay widths, form factors, or isospin-breaking dynamics beyond charged vs neutral mass ordering.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.KaonMasses module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (29)

def pionChargedMass_MeV L48
def pionNeutralMass_MeV L51
def pionChargedMass_eV L54
def pionNeutralMass_eV L57
def pionRung L63
def mesonBinaryGauge L66
def pionMassPredicted_eV L69
def electronMass_eV L73
def pionElectronRatio L76
def pionElectronRatioPredicted L79
theorem pion_mass_near_140 L84
theorem charged_heavier_than_neutral L89
theorem pion_electron_ratio_approx L94
theorem phi_12_div_2 L101
def phi_12 L136
def pionMassDifference_MeV L141
theorem mass_difference_electromagnetic L144
def relativeMassDifference L150
theorem relative_difference_about_3_percent L152
def lightQuarkMass_MeV L164
def pionDecayConstant_MeV L167
def quarkCondensate_MeV L170
def gmorPrediction L173
theorem gmor_reasonable L177
def pionSpin L186
def pionIsospin L187
def pionParity L190
def pionMultiplet L193
theorem pion_triplet_mod L196