dm2_21_frac_pred
plain-language theorem explainer
The definition supplies the model's prediction for the solar neutrino mass-squared splitting under the fractional rung assignment on the deep ladder. Oscillation data analysts and neutrino mass modelers cite it when benchmarking the Recognition Science ladder against NuFIT measurements. It is realized as a direct one-line application of the mass-squared difference operator to the legacy-calibrated eV predictions for the two lightest neutrino states.
Claim. The predicted solar neutrino mass-squared splitting is given by $Δm_{21}^2 = m_2^2 - m_1^2$, where $m_2$ and $m_1$ are the eV-scale masses obtained from the legacy fractional-rung calibration applied to the solar and lightest neutrino rungs.
background
The neutrino sector module places neutrinos on the deep ladder at even-integer rungs near -54 and -58, with the structural mass scale obtained by treating the electron structural mass as a MeV quantity and converting by $10^6$. The dm2 operator is the difference of squares of two real masses. The rung res_nu2 is obtained by subtracting the nu_spacing from res_nu3, while res_nu1 subtracts the quarter-cycle spacing nu1_spacing from res_nu2, enforcing the 8-tick periodicity.
proof idea
This is a one-line wrapper that applies the dm2 definition to the outputs of predicted_mass_eV_frac on res_nu2 and res_nu1 under the legacy calibration.
why it matters
The definition supplies the concrete value fed to NeutrinoMassScaleScoreCardCert and to the lemma dm2_21_frac_pred_in_nufit_1sigma that checks consistency with the NuFIT 1σ interval. It completes the T14 derivation of the neutrino mass scale from the phi-ladder and eight-tick octave, anchoring the solar scale prediction inside the observed band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.