gmo_relation_approximate
plain-language theorem explainer
The theorem verifies that the Gell-Mann-Okubo mass relation holds approximately for the charged kaon, eta, and charged pion, with relative discrepancy below 10 percent. Particle physicists comparing meson octet predictions to PDG data would cite this numerical check inside the kaon masses derivation. The proof is a direct term reduction that substitutes the four mass constants and evaluates the inequality by arithmetic normalization.
Claim. Let $m_K = 493.677$ MeV, $m_η = 547.862$ MeV, and $m_π = 139.57039$ MeV. Then $|4 m_K^2 - (3 m_η^2 + m_π^2)| / (4 m_K^2) < 0.1$.
background
The module derives kaon masses from Recognition Science by placing the strange quark on a higher rung of the phi-ladder than the light quarks in pions. The Gell-Mann-Okubo relation for the pseudoscalar octet is stated as the approximate identity 4 m_K² = 3 m_η² + m_π². gmo_lhs is defined as 4 times the square of the charged kaon mass; gmo_rhs is defined as 3 times the square of the eta mass plus the square of the charged pion mass. etaMass_MeV supplies the numerical value 547.862 MeV while kaonChargedMass_MeV and pionChargedMass_MeV supply the remaining constants.
proof idea
The term proof applies simp only to unfold gmo_lhs, gmo_rhs, kaonChargedMass_MeV, etaMass_MeV, and pionChargedMass_MeV, then closes with norm_num to evaluate the resulting arithmetic expression and confirm the strict inequality.
why it matters
The declaration supplies a concrete numerical anchor for the approximate GMO relation inside the kaon masses derivation (P-014). It sits downstream of the mass constant definitions and supports the module's claim that kaon masses follow phi-ladder patterns under SU(3) flavor symmetry. No downstream theorems currently depend on it, leaving the check as a self-contained verification step rather than a lemma for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.