row_nu1_frac
plain-language theorem explainer
The declaration supplies the numerical interval 0.00352 to 0.00355 for the predicted fractional mass of the lightest neutrino rung in eV units. Neutrino mass modelers working inside the Recognition Science phi-ladder framework cite the bound when populating the scorecard certificate. The proof is a direct one-line wrapper that invokes the upstream lemma nu1_frac_pred_bounds without further reduction.
Claim. $0.00352 < m_1 < 0.00355$, where $m_1$ is the default fractional-rung mass prediction in eV for the lightest neutrino rung res_nu1 placed two rungs below res_nu2 under the legacy mass display calibration.
background
The NeutrinoMassScaleScoreCard module packages Phase 2 neutrino mass predictions that combine fractional rung placement on the phi-ladder with NuFIT windows for squared-mass splittings. The definition predicted_mass_eV_frac res applies the legacy mass display calibration to the structural mass of any given rung. The rung res_nu1 is obtained by subtracting nu1_spacing from res_nu2, implementing the parameter-free eight-tick quarter placement for the lightest neutrino.
proof idea
The proof is a one-line wrapper that directly applies the lemma nu1_frac_pred_bounds. That lemma unfolds predicted_mass_eV_frac_legacy together with MeV_to_eV and legacy_mass_display_calibration, then invokes ElectronMass.Necessity.structural_mass_bounds and the equality phi = Real.goldenRatio.
why it matters
The bound populates the nu1_frac field inside the NeutrinoMassScaleScoreCardCert structure whose non-emptiness is established by neutrinoMassScaleScoreCardCert_holds. It forms part of the packaged scorecard for the P2-ν phase that includes the structural equality m_3²/m_2² = phi^7. The result sits inside the Recognition Science forcing chain where the eight-tick octave and phi-ladder fix the neutrino rung assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.