row_dm2_31_nufit
plain-language theorem explainer
Neutrino phenomenologists cite the result when verifying that the Recognition Science fractional rung model places the squared mass splitting Δm²₃₁ inside the NuFIT 5.2 2σ band from 2.455×10^{-3} to 2.567×10^{-3}. The bound is required to assemble the neutrino mass scale scorecard certificate. The proof is a one-line wrapper invoking the upstream lemma that establishes the same numerical interval.
Claim. The fractional-rung prediction for the neutrino squared mass splitting satisfies $2.455×10^{-3} < Δm_{31}^2 < 2.567×10^{-3}$, where the splitting is obtained from the difference of the predicted fractional masses of the third and first neutrino eigenstates.
background
The module treats Phase 2 neutrino mass scale predictions via fractional rung placement on the phi-ladder together with NuFIT bands for squared splittings. The quantity is defined as the dm2 of the predicted fractional masses for the third and first neutrino rung assignments. The upstream lemma already proves the identical bounds by applying the individual rung bounds for the third and first neutrinos. This row simply re-exports the result inside the scorecard module for downstream certificate construction.
proof idea
The proof is a one-line wrapper that applies the lemma dm2_31_frac_pred_in_nufit_2sigma.
why it matters
This bound supplies the Δm²₃₁ entry in the neutrinoMassScaleScoreCardCert_holds theorem, which packages all fractional rung predictions and NuFIT windows into a single nonempty certificate. It verifies compatibility of the φ^7 structural mass-ratio model with oscillation data in the Phase 2 neutrino sector. The module documentation states that a NuFit/PDG update placing either Δm² outside the proved windows would falsify the packaged splitting certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.