nu_spacing_eq
plain-language theorem explainer
The lemma establishes that the neutrino spacing equals seven halves in the rational numbers. Researchers deriving neutrino masses on the Recognition Science phi-ladder cite this to fix the solar-to-atmospheric rung gap. The proof is a one-line wrapper that unfolds the spacing definition and normalizes the arithmetic.
Claim. $nu_{spacing} = 7/2$
background
The NeutrinoSector module places neutrinos on the deep phi-ladder with rungs far below the electron at R=2. The spacing is defined as ((8 : Q) - 1)/2 to capture the gap between atmospheric (R=-54) and solar (R=-58) scales after residue adjustment. Upstream rung definitions assign nu3 to 19 and nu2 to 11 in the RSBridge anchor, with the module noting a quarter-ladder structure for the residue difference of 4.
proof idea
The proof is a one-line wrapper. It unfolds nu_spacing and applies norm_num to reduce ((8-1)/2) directly to 7/2.
why it matters
This lemma is invoked by rung_gap_is_seven_halves to prove the exact 7/2 gap between res_nu3 and res_nu2, and by res_nu2_simp for residue simplification. It supplies the spacing detail required by the T14 neutrino hypothesis, where masses follow the phi-ladder formula m_struct * phi^rung and the 7/2 gap yields a squared-mass ratio of phi^7. The result anchors the eight-tick octave structure in the neutrino sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.