nu2_frac_pred_bounds
plain-language theorem explainer
The lemma proves that the predicted mass in eV for the second neutrino generation at residue res_nu2 lies strictly between 0.00924 and 0.00928. Neutrino mass modelers working in the Recognition Science framework cite it to confirm the solar-scale phi-ladder prediction aligns with oscillation data. The tactic proof unfolds the legacy calibration, pulls electron structural mass bounds and phi^{-231/4} interval bounds, rewrites the exponent, then chains two calc blocks with nlinarith to sandwich the scaled product.
Claim. $0.00924 < m_2 < 0.00928$, where $m_2$ is the predicted mass in eV for the second neutrino obtained by scaling the structural electron mass by $phi^{-231/4}$ under the legacy MeV-to-eV display calibration.
background
The NeutrinoSector module derives neutrino masses on the deep phi-ladder, with nu2 at residue res_nu2 corresponding to exponent -231/4. electron_structural_mass is defined as lepton_yardstick * phi^(electron_rung - octave_period) and satisfies 10856 < electron_structural_mass < 10858 by structural_mass_bounds. legacy_mass_display_calibration treats this quantity as MeV and multiplies by 10^6 to report in eV. phi_neg2314_gt and phi_neg2314_lt supply the tight interval 8.514e-13 < goldenRatio^{-231/4} < 8.538e-13. toReal transports the residue to the real line. This sits inside the T14 neutrino sector formalization that posits quarter-rung spacing for the deep ladder.
proof idea
The proof simplifies predicted_mass_eV_frac res_nu2 via predicted_mass_eV_frac_legacy, MeV_to_eV and legacy_mass_display_calibration. It obtains structural_mass_bounds, phi_neg2314_gt and phi_neg2314_lt. After rewriting phi to goldenRatio and the exponent of res_nu2 to -231/4 via toReal and res_nu2_simp, positivity of the structural mass and the power term is established. Two separate calc blocks then apply nlinarith with the imported bounds to prove the lower and upper inequalities independently.
why it matters
The lemma is invoked verbatim by row_nu2_frac in NeutrinoMassScaleScoreCard and supplies the key bound for dm2_21_frac_pred_in_nufit_1sigma, which checks the fractional solar Delta m^2 against NuFIT 1-sigma. It completes the m2 prediction inside T14, using the phi-ladder mass formula and the eight-tick octave structure. The numerical interval supports the quarter-ladder spacing hypothesis for neutrino generations while remaining inside the legacy calibration seam.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.