dm2_21_frac_pred_with
plain-language theorem explainer
dm2_21_frac_pred_with supplies a calibration-dependent expression for the solar neutrino mass-squared splitting Δm²₂₁ in the fractional rung model. Neutrino physicists modeling masses on the phi-ladder would cite this when comparing RS predictions to oscillation data. The definition is a one-line wrapper that feeds the calibrated fractional masses for the second and first neutrino states into the dm2 difference operator.
Claim. For a calibration parameter $c$ the predicted fractional solar splitting is $dm2(m_2(c), m_1(c))$, where $m_i(c)$ denotes the eV-scale mass obtained by applying the display scaling of $c$ to the structural mass at the rung assigned to neutrino generation $i$.
background
The neutrino sector module assigns neutrinos to deep negative rungs on the phi-ladder: rung -54 for the atmospheric scale and rung -58 for the solar scale, with residue difference Δ₃₂ = 4. MassDisplayCalibration is the structure that supplies an explicit positive scaling factor eV_per_structural_unit to convert the dimensionless RS structural mass into reported eV values; the module doc notes that this is a reporting seam, not a parameter-free derivation, and reuses the electron structural mass treated as MeV before the MeV_to_eV conversion. The definition therefore parameterizes the Δm²₂₁ computation so different display conventions can be substituted while the underlying rung assignments remain fixed. Upstream results include the dm2 operator and the predicted_mass_eV_frac_with function that applies the chosen calibration to individual rung masses.
proof idea
This is a one-line wrapper that applies the dm2 difference operator to the two outputs of predicted_mass_eV_frac_with evaluated at the supplied calibration for res_nu2 and res_nu1.
why it matters
The definition feeds the legacy form dm2_21_frac_pred_with_legacy and the NuFIT 1σ interval check dm2_21_frac_pred_with_legacy_in_nufit_1sigma. It completes the T14 neutrino sector derivation by allowing flexible reporting of the phi-ladder mass predictions for Δm²₂₁ while keeping the structural mass scale separate from the display calibration. In the Recognition framework it supports direct comparison of the rung spacing against oscillation data inside the eight-tick octave and D = 3 setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.