module module moderate

`IndisputableMonolith.Physics.KaonMasses`

The KaonMasses module supplies RS-derived definitions for charged and neutral kaon masses in MeV together with ratios to pions and electrons. Particle physicists applying Recognition Science to meson spectra would cite these for extensions beyond the pion sector. The module is a collection of direct definitions and numerical approximations that reuse the phi-ladder and prior pion results.

claim$m_{K^\pm}$ and $m_{K^0}$ in MeV, with kaon-pion ratio near $\\,\phi^2 + 1$ and kaon-electron ratio, using the mass formula on the phi-ladder.

background

Constants supplies the RS time quantum $\tau_0 = 1$ tick. PhiForcing proves that $\phi$ is forced as the self-similar fixed point of the discrete ledger obeying the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. PionMasses derives the lightest mesons as quark-antiquark bound states on the same ladder.

KaonMasses extends the same mechanism to strange mesons, defining masses via the yardstick $\times \phi^{rung-8+gap(Z)}$ expression and recording PDG 2024 reference values for the charged kaon.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module populates the phi-ladder for hadrons with strangeness, supplying concrete mass values that later derivations in the physics layer can reference. It applies T6 (phi fixed point) and the mass formula directly to the kaon sector after the pion results, closing one rung of the meson spectrum within the eight-tick octave framework.

scope and limits

Does not derive kaon masses from first principles without pion inputs.
Does not include decay rates or interaction vertices.
Does not claim exact numerical equality beyond the listed approximations.
Does not address higher-order QFT corrections or running couplings.

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