module module moderate

`IndisputableMonolith.Physics.KaonMasses`

KaonMasses supplies numerical values and phi-based approximations for charged and neutral kaon masses in MeV together with pion and electron ratios. Researchers deriving meson spectra inside Recognition Science would cite the module for the strange sector. It consists of direct definitions and near-equality statements that extend the imported pion and phi modules without further derivation steps.

claimThe module states $m_{K^+} = m_{K^-} = 493.677$ MeV (PDG 2024), $m_{K^0} > m_{K^+}$ with difference near 3.97 MeV, and the ratio $m_K / m_π ≈ φ² + 1$ where φ is the golden ratio forced by self-similarity.

background

The module sits inside the Recognition Science derivation of particle masses. It imports the base time quantum τ₀ = 1 tick from Constants, the forcing of φ as self-similar fixed point in a discrete ledger with J-cost from PhiForcing, and the pion masses obtained from quark-antiquark binding from PionMasses. Kaons are treated as the next rung on the phi-ladder once the strange quark is introduced.

proof idea

This is a definition module, no proofs. The listed approximations are direct numerical statements or immediate comparisons taken from the phi-ladder relations already established in the imported modules.

why it matters in Recognition Science

The module extends the pion mass work (P-013) into the strange sector, supplying the kaon values and ratios required by any later RS calculation of meson spectra or quark masses. It therefore sits between the foundational phi forcing and higher-level particle phenomenology inside the framework.

scope and limits

Does not derive kaon masses from the full J-cost ledger without PDG anchors.
Does not treat kaon decays, lifetimes, or interaction vertices.
Does not prove that the listed numerical assignments are the only possible RS values.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Physics.PionMasses module_import

declarations in this module (27)

def kaonChargedMass_MeV L49
def kaonNeutralMass_MeV L52
def strangeQuarkMass_MeV L55
def kaonPionRatio L60
def kaonElectronRatio L63
theorem kaon_mass_near_494 L68
theorem neutral_heavier_than_charged L73
theorem kaon_pion_ratio_approx L78
def phi_2_6 L85
theorem kaon_pion_near_phi_sq_plus_1 L92
def kaonMassDifference_MeV L114
theorem kaon_mass_difference_approx L117
def etaMass_MeV L126
def gmo_lhs L129
def gmo_rhs L130
theorem gmo_relation_approximate L132
def kLongMass_MeV L143
def kShortMass_MeV L146
def kLkS_massDifference L149
def kLongLifetime L152
def kShortLifetime L155
theorem lifetime_ratio L158
def kaonDoublets L167
def kaonDoubletSize L170
def totalKaons L173
theorem total_kaons_is_4 L175
theorem eight_div_2 L178