row_nu2_frac
plain-language theorem explainer
The declaration establishes that the predicted fractional mass for the second neutrino rung satisfies 0.00924 < predicted_mass_eV_frac res_nu2 < 0.00928 in RS-native units. Neutrino mass modelers cite the bound when assembling the scorecard for the neutrino sector against NuFIT windows. The proof is a direct one-line application of the upstream lemma nu2_frac_pred_bounds.
Claim. $0.00924 < m_2 < 0.00928$, where $m_2$ is the default fractional-rung prediction in eV for the solar neutrino rung res_nu2 (defined by enforcing rung spacing $r_3 - r_2 = 7/2$).
background
The module treats Phase 2 neutrino mass scale via fractional ladder placement, NuFIT bands for squared splittings, and the structural relation $m_3^2/m_2^2 = phi^7$ under the res_nu3 - res_nu2 = 7/2 model. The definition predicted_mass_eV_frac computes the default fractional-rung prediction in eV under legacy convention as predicted_mass_eV_frac_with legacy_mass_display_calibration res. The rung res_nu2 is defined as res_nu3 minus nu_spacing, where nu_spacing is one quarter of the 8-tick cycle.
proof idea
The proof is a one-line wrapper that applies the lemma nu2_frac_pred_bounds. That lemma reduces the target inequality by simp on predicted_mass_eV_frac_legacy, MeV_to_eV and legacy_mass_display_calibration, then invokes structural_mass_bounds together with the numeric bounds phi_neg2314_gt and phi_neg2314_lt.
why it matters
The bound is collected into neutrinoMassScaleScoreCardCert_holds, which packages the full NeutrinoMassScaleScoreCardCert. It supplies the eV-scale fractional mass entry for the solar rung and thereby supports the P2-ν structural phi^7 mass-ratio equality stated in the module documentation. The result closes one cell of the scorecard while leaving absolute eV calibration to the shared seam with NeutrinoSector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.