dm2_31_frac_pred_with_legacy
plain-language theorem explainer
The lemma shows that the fractional prediction for atmospheric neutrino mass-squared difference remains identical under the legacy mass display calibration. Neutrino mass modelers working with the phi-ladder would cite it to confirm that calibration choice does not shift the central value. The proof is a direct term-mode simplification that unfolds the wrapped and unwrapped prediction definitions together with the fractional mass expression.
Claim. The fractional prediction for the atmospheric neutrino mass-squared splitting computed with the legacy display calibration equals the standard fractional prediction: $dm^2_{31, frac, legacy} = dm^2_{31, frac}$.
background
The neutrino sector module places the three neutrino masses on deep negative rungs of the phi-ladder, with the atmospheric scale at rung -54 and the solar scale at rung -58. Masses are obtained from the structural yardstick scaled by negative powers of phi, then converted to eV via a display convention that treats the electron structural mass as if measured in MeV. The legacy calibration reuses the electron structural mass directly with the MeV-to-eV factor, creating a reporting seam rather than a parameter-free derivation.
proof idea
One-line wrapper that applies simp to unfold the legacy-wrapped prediction, the base prediction, and the fractional mass computation, establishing syntactic equality of the two expressions.
why it matters
The result feeds the downstream NuFIT 2-sigma consistency lemma, preserving the proved interval bound when the legacy calibration is active. It supports the T14 hypothesis that neutrino scales arise from deep-ladder rung spacing of four units, consistent with the Recognition Science phi-ladder mass formula and the eight-tick octave structure. The module documentation flags the calibration seam as the point where absolute eV reporting is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.