kaon_mass_difference_approx
plain-language theorem explainer
The declaration verifies that the neutral minus charged kaon mass difference equals 3.934 MeV and therefore lies inside the interval (3.8, 4.0) MeV. Physicists comparing Recognition Science mass ladders to PDG data would cite the numerical check when validating the strange-quark rung placement. The proof is a one-line wrapper that unfolds the three mass constants and hands the resulting arithmetic inequality to norm_num.
Claim. $|(m_{K^0} - m_{K^+}) - 3.9| < 0.1$ (masses in MeV).
background
Kaon masses are derived in the Recognition Science framework by placing the strange mesons on a higher rung of the phi-ladder than the pions. The module records the experimental inputs K^+ mass = 493.677 MeV and K^0 mass = 497.611 MeV from PDG 2024, yielding the difference 3.934 MeV. Upstream definitions supply these constants directly as real numbers.
proof idea
The term-mode proof applies the simp tactic to unfold the definitions of kaonMassDifference_MeV as the subtraction of kaonNeutralMass_MeV minus kaonChargedMass_MeV, then invokes norm_num to discharge the resulting numerical inequality.
why it matters
This result supplies a concrete numerical anchor for the kaon mass splitting predicted by Recognition Science. It confirms the module's stated approximation of 3.9 MeV and aligns with the phi-ladder placement for strange quarks. No downstream theorems depend on it, so it functions as a standalone verification of the mass difference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.