m3_approx_bounds
plain-language theorem explainer
The lemma establishes that the approximate third neutrino mass, defined as the square root of the experimental atmospheric mass-squared splitting 2.453e-3, satisfies 0.049 < m3_approx < 0.050 in eV. Neutrino modelers working inside the Recognition Science phi-ladder framework cite the bound to anchor the atmospheric scale to rung -54. The proof reduces both sides to squared comparisons via norm_num, then invokes monotonicity of the positive square root to conclude the original inequalities.
Claim. $0.049 < m_3^approx < 0.050$ where $m_3^approx = sqrt(2.453 times 10^{-3})$ in eV and the experimental input is the atmospheric mass-squared difference $Delta m_{32}^2$.
background
The NeutrinoSector module places neutrinos on deep negative rungs of the phi-ladder, with the atmospheric scale assigned to rung -54. The definition dm2_32_exp supplies the numerical anchor 2.453e-3 (in eV squared) drawn from experiment, and m3_approx is obtained by taking its positive square root under the approximation that the lightest neutrino mass is negligible. These quantities appear after a reporting convention that re-uses the electron structural mass (dimensionless in RS-native units) as if expressed in MeV and multiplies by 10^6 to reach eV display units.
proof idea
simp unfolds m3_approx and dm2_32_exp. constructor splits the conjunction. The lower bound is proved by showing 0.049 squared is less than 0.002453 (norm_num), rewriting the target as a comparison of square roots, and applying Real.sqrt_lt_sqrt. The upper bound proceeds symmetrically by comparing 0.002453 to 0.050 squared and again using the monotonicity of sqrt on the non-negative reals.
why it matters
The bound is invoked inside nu3_match to verify that the predicted mass at rung -54 (approximately 0.056 eV) lies within 0.01 eV of the approximate observed value. It therefore closes one numerical check in the T14 neutrino-sector derivation, confirming consistency between the phi-ladder mass formula and the measured atmospheric Delta m squared. The result sits downstream of the rung assignment for nu3 and upstream of any global mass-scale calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.