res_nu3_simp
plain-language theorem explainer
The lemma fixes the upgraded atmospheric neutrino rung at the rational value -217/4. Neutrino mass derivations in the Recognition framework cite it to anchor the fractional phi-ladder position for the atmospheric scale before applying the structural mass calibration. The proof is a direct term reduction that unfolds the residue definition and substitutes the integer rung together with the independently established quarter-phase offset.
Claim. The upgraded atmospheric neutrino residue satisfies $r_3 = -217/4$.
background
The Neutrino Sector module places neutrinos on the deep ladder at large negative integer rungs. rung_nu3 is the base integer -54 for the atmospheric scale. nu_phase_offset is the fixed quarter offset -1/4. res_nu3 is defined as ofInt rung_nu3 plus this offset, producing the effective fractional rung used for mass predictions after calibration to the electron structural mass in MeV then converted to eV.
proof idea
One-line wrapper that unfolds res_nu3, substitutes rung_nu3 = -54 and the value from nu_phase_offset_eq, then reduces with norm_num to obtain the rational -217/4.
why it matters
This lemma supplies the exact rational rung required by nu3_frac_pred_bounds to close the interval (0.04985, 0.04993) eV and by res_nu2_simp to derive the solar rung via the 7/2 spacing. It completes the T14 neutrino sector step in the Recognition framework by locking the phi-ladder position for m3 consistent with the self-similar fixed point and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.