rung_gap_21_is_two
plain-language theorem explainer
rung_gap_21_is_two establishes that the residue difference between the second and first neutrino generations equals exactly two. Neutrino mass modelers in the Recognition Science framework cite it when fixing the solar scale spacing on the phi-ladder. The proof reduces directly by unfolding the definition of res_nu1 and simplifying against the nu1 spacing equation.
Claim. The residue of the second neutrino minus the residue of the first neutrino equals two: $r_2 - r_1 = 2$.
background
The NeutrinoSector module derives neutrino masses from the deep ladder hypothesis in Recognition Science, placing the atmospheric scale at rung -54 and the solar scale at rung -58 on the phi-ladder. Residues res_nu1 and res_nu2 capture the effective positions for the first and second neutrino mass eigenstates after structural mass scaling, reported in eV via a display convention that treats the electron structural mass as if measured in MeV before applying the MeV_to_eV conversion factor.
proof idea
The proof unfolds the definition of res_nu1 and applies simplification using the nu1_spacing_eq lemma, which directly yields the difference of two.
why it matters
This result supplies a precise residue step for the solar neutrino mass prediction m2 in the T14 neutrino sector derivation. It aligns with the phi-ladder mass formula and the rung assignments from upstream anchor policies, supporting the observed Delta m squared 21 scale without introducing new parameters. The module documentation notes the quarter-ladder structure with spacing of four for the 32 sector, making this two-unit gap for the 21 sector a consistent subcase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.