module module high

`IndisputableMonolith.Physics.PionMasses`

PionMasses supplies RS-native constants for charged and neutral pion masses in MeV and eV, plus rung assignments on the phi-ladder and predicted electron-mass ratios. A particle physicist checking Recognition Science outputs against PDG tables would cite these values. The module is a pure definition collection that pulls numerical yardsticks from Constants and phi-forcing structure from PhiForcing.

claimThe module defines $m_{π^±} = 139.57$ MeV, $m_{π^0} = 134.98$ MeV (PDG 2024), their eV equivalents, the rung index on the phi-ladder, the binary gauge for mesons, and the predicted ratio $m_π / m_e$ together with its RS value.

background

The module sits inside the Physics domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the self-similar ledger that forces φ from PhiForcing. Pion masses are expressed via the mass formula yardstick × φ^(rung − 8 + gap(Z)) on the phi-ladder, using the mesonBinaryGauge and pionRung siblings. The charged-neutral split is carried by the defectDist term inherited from the J-cost structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

PionMasses supplies the light-meson inputs required by the downstream KaonMasses module (P-014), which extends the same ladder to strange quarks. It therefore anchors the non-strange sector of the meson spectrum before the eight-tick octave and D = 3 forcing steps are applied to heavier states.

scope and limits

Does not derive the mass formula from the J-cost ledger.
Does not compute decay rates or coupling constants.
Does not address isospin violation beyond the charged-neutral mass difference.
Does not extend the ladder to vector or heavier mesons.

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