kaon_pion_ratio_approx
plain-language theorem explainer
The charged kaon to charged pion mass ratio lies within 0.01 of 3.54. Modelers of meson spectra under Recognition Science cite this bound when placing kaons on the phi-ladder. The proof unfolds the ratio definition into explicit PDG constants and checks the inequality by direct numerical evaluation.
Claim. $ | m_{K^+} / m_π^+ - 3.54 | < 0.01 $
background
In the Kaon Masses module the ratio is defined directly as the quotient of the charged kaon mass (493.677 MeV) and the charged pion mass (139.57039 MeV). Kaons sit on a higher rung of the phi-ladder because they contain one strange quark whose mass dominates the light-quark contributions. The module derives these masses from Recognition Science by combining strange-quark content, SU(3) flavor symmetry, and the Gell-Mann-Okubo mass formula, yielding the explicit prediction that the ratio approximates 3.54 and therefore φ^2.6.
proof idea
The proof is a one-line wrapper. It applies simp to substitute the three definitions kaonPionRatio, kaonChargedMass_MeV and pionChargedMass_MeV, then invokes norm_num to evaluate the absolute difference against the constant 3.54.
why it matters
The declaration supplies the numerical check required by the Kaon Masses Derivation (P-014) that m_K/m_π ≈ 3.54 ≈ φ^2.6. It therefore anchors the phi-ladder placement of strange mesons inside the Recognition framework and closes one concrete instance of the mass formula yardstick · φ^(rung-8+gap(Z)). No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.