row_nu3_frac
plain-language theorem explainer
The theorem certifies that the predicted fractional mass in eV for the atmospheric neutrino rung lies strictly between 0.04985 and 0.04993. Neutrino mass modelers checking Recognition Science predictions against NuFIT data cite this bound to anchor the phi-ladder placement. The proof is a one-line wrapper that invokes the upstream interval lemma from the NeutrinoSector module.
Claim. $0.04985 < m_3^{frac} < 0.04993$, where $m_3^{frac}$ is the predicted mass in eV for the upgraded atmospheric neutrino rung whose squared-mass ratio to the solar rung equals $φ^7$.
background
The module treats Phase 2 neutrino mass scale via fractional rung placement on the phi-ladder together with NuFIT bands for squared splittings and the structural relation $m_3^2/m_2^2 = φ^7$. The rung res_nu3 is the integer base plus quarter-phase offset that enforces the exact 7/2 gap with the solar rung. The function predicted_mass_eV_frac returns the default fractional-rung mass in eV under legacy calibration.
proof idea
The proof is a one-line wrapper that directly applies the lemma nu3_frac_pred_bounds from NeutrinoSector, which itself unfolds the reporting seam and invokes structural mass bounds plus phi-power inequalities.
why it matters
This bound populates the NeutrinoMassScaleScoreCardCert that packages all fractional predictions and NuFIT comparisons for the neutrino sector. It thereby closes the re-exported interval part of the partial theorem on rung-gap structure and φ^7 mass ratio stated in the module documentation. The result sits inside the Recognition Science forcing chain at the T5 J-uniqueness and T6 phi fixed-point steps applied to the neutrino ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.