module module moderate

`IndisputableMonolith.Physics.KaonMasses`

This module supplies RS-derived numerical values and phi-based approximations for charged and neutral kaon masses in MeV, plus the strange quark mass, mass differences, and ratios to pions and electrons. Hadron physicists would cite it when checking Recognition Science predictions against PDG data. The module is a collection of definitions and near-equalities that extend the pion mass results using the phi-ladder.

claimThe charged kaon mass $m_{K^+} ext{ (MeV)}$, neutral kaon mass $m_{K^0} ext{ (MeV)}$, strange quark mass, kaon-pion ratio $m_K/m_\\pi$, kaon-electron ratio, and mass difference $m_{K^0}-m_{K^+}$ are defined with values near 494 MeV and approximations involving $\phi^{2.6}$ and $\phi^2+1$.

background

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

KaonMasses applies the same RS mass formula (yardstick times $\phi$ to a rung adjusted by gap) to the strange sector, defining the listed kaon quantities as extensions of the pion results.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module extends PionMasses into the strange-quark sector and supplies kaon mass inputs for the Recognition Science mass formula. It connects to the T5 J-uniqueness and T6 phi fixed-point steps, plus the eight-tick octave and D=3 spatial dimensions. No direct downstream theorems are listed.

scope and limits

Does not derive kaon masses from the full unified forcing chain T0-T8 without external PDG anchors.
Does not address kaon decays, mixing, or CP violation.
Does not claim exact equality to experiment beyond the listed near-equalities.
Does not compute the alpha band or G constant from these masses.

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