res_nu1_simp
plain-language theorem explainer
The lemma fixes the numerical residue of the lightest neutrino rung at -239/4 in quarter-ladder units. Neutrino mass modelers cite it when anchoring the solar scale two rungs below the atmospheric one on the phi-ladder. The proof is a term-mode reduction that unfolds the definition and substitutes the already-simplified solar residue together with the quarter-cycle spacing equality.
Claim. The residue rung for the lightest neutrino satisfies $r_{nu1} = -239/4$.
background
The NeutrinoSector module places neutrinos on the deep ladder at even negative rungs far below the electron. Mass 3 sits near rung -54 and mass 2 near rung -58, with the residue difference between generations fixed at 4. The definition res_nu1 is the upgraded lightest rung obtained by subtracting nu1_spacing from res_nu2, where nu1_spacing is the canonical quarter of the 8-tick cycle and equals 2. Upstream, nu1_spacing_eq states that this spacing is exactly 2, while res_nu2_simp already fixes the solar residue at -231/4.
proof idea
The proof is a one-line term-mode wrapper. It unfolds res_nu1 to the difference res_nu2 minus nu1_spacing, then applies the simplifications res_nu2_simp and nu1_spacing_eq before normalizing the rational arithmetic.
why it matters
This simplification closes the rung assignment for the lightest neutrino in the T14 derivation. It supplies the concrete value needed for the mass approximations m2_approx and m3_approx and for the display calibrations in the same module. The construction rests on the eight-tick octave (T7) that forces the quarter-ladder spacing of 2 rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.