m3_approx
plain-language theorem explainer
The definition m3_approx extracts the atmospheric neutrino mass scale by taking the positive square root of the experimental squared-mass difference dm2_32_exp. Neutrino physicists matching Recognition Science phi-ladder predictions to oscillation data cite this quantity when bounding the m3 rung. It is realized as a direct one-line definition that applies the real square root to the supplied experimental constant.
Claim. $m_3^approx := sqrt(Delta m_{32}^{2,exp})$, where $Delta m_{32}^{2,exp} = 2.453 times 10^{-3}$ eV$^2$ (assuming $m_1 approx 0$).
background
In the Recognition Science neutrino sector (T14), neutrinos occupy the deep ladder at even negative rungs far below the electron scale $R_e=2$. The module treats the atmospheric scale as rung -54, with the experimental input dm2_32_exp supplying the squared mass difference 2.453e-3 eV^2 from which the mass scale is extracted. The upstream definition dm2_32_exp is documented as providing approximate masses assuming m1 ~ 0.
proof idea
This is a one-line definition that applies Real.sqrt directly to dm2_32_exp.
why it matters
This definition supplies the experimental mass scale compared against the structural prediction in nu3_match and packaged inside NeutrinoMassCert. It closes the loop between the phi-ladder mass formula and observed atmospheric oscillations in the T14 sector, verifying that rung -54 yields a value within 0.01 eV of the extracted scale. The module notes that absolute eV reporting remains a calibration seam rather than a parameter-free derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.