dm2
plain-language theorem explainer
This definition supplies the squared mass difference between two neutrino mass eigenstates as the difference of their squares. Neutrino modelers in the Recognition Science setting cite it to build the solar and atmospheric splittings from rung-predicted masses. The body is a direct one-line subtraction of squares in the reals.
Claim. The mass-squared splitting is defined by $Δm^2(m_hi, m_lo) := m_hi^2 - m_lo^2$.
background
The NeutrinoSector module places neutrinos on the deep phi-ladder at even rungs near -54 for the atmospheric scale and -58 for the solar scale, with masses obtained by scaling the structural mass by phi to those powers and converting via the electron-mass calibration seam. The module treats the eV reporting as a display convention that reuses the dimensionless electron structural mass as if in MeV and multiplies by 10^6. This definition supplies the operator that turns pairs of rung masses into the observable Δm² values.
proof idea
One-line definition that subtracts the square of the lower mass from the square of the higher mass.
why it matters
It is the common operator inside dm2_21_frac_pred, dm2_31_frac_pred and their calibration-parameterized variants, which are then checked against NuFIT 1σ and 2σ bands in the lemmas dm2_21_frac_pred_in_nufit_1sigma and dm2_31_frac_pred_in_nufit_2sigma. The definition therefore realizes the T14 neutrino-sector hypothesis that the rung spacing of 4 is consistent with the phi-ladder mass formula and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.