m2_approx
plain-language theorem explainer
Approximate solar neutrino mass scale obtained by taking the square root of the experimental squared-mass difference under the assumption that the lightest neutrino mass vanishes. Recognition Science neutrino-sector derivations cite this quantity when matching the phi-ladder prediction at rung -58 to observed solar oscillations. The definition performs a direct square-root extraction from the fixed experimental input 7.53e-5 eV².
Claim. $m_2^approx := sqrt(Delta m_{21,exp}^2)$ where the experimental input $Delta m_{21,exp}^2 = 7.53 times 10^{-5}$ eV² encodes the solar oscillation scale.
background
In the Recognition Science neutrino sector, neutrinos occupy the deep phi-ladder at large negative integer rungs far below the electron rung. The solar scale is assigned rung -58, so the structural mass scaled by phi^{-58} yields a predicted mass near 0.0082 eV after the module's display calibration that treats the dimensionless electron structural mass as if measured in MeV and multiplies by 10^6. The upstream anchor dm2_21_exp supplies the experimental squared-mass difference 7.53e-5 eV² that encodes the oscillation frequency between the second and first mass eigenstates.
proof idea
One-line definition that applies the real square-root function directly to dm2_21_exp.
why it matters
This quantity supplies the experimental target for the solar neutrino mass match inside T14. It is used by m2_approx_bounds to certify the interval (0.0086, 0.0088) eV, by nu2_match to verify agreement with the rung -58 prediction to within 0.001 eV, and by the NeutrinoMassCert structure that packages both atmospheric and solar certificates. The construction links the Recognition Composition Law to the observed oscillation scales on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.