nu1_spacing_eq
plain-language theorem explainer
The lemma fixes the rung spacing between the lightest neutrino and the next generation at exactly two units on the Recognition Science phi-ladder. Neutrino mass modelers would cite this when deriving solar and atmospheric scales from the deep ladder residues. The proof is a direct unfolding of the spacing definition followed by numerical normalization to the constant 2.
Claim. The spacing parameter between the first and second neutrino rungs on the phi-ladder satisfies spacing = 2 in the rationals.
background
The NeutrinoSector module derives neutrino masses from the deep ladder, where masses scale as structural mass times phi to negative integer rungs far below the electron rung of 2. The rung function assigns integer positions to fermions, with neutrinos at low values such as 0 for nu1 and 11 for nu2 in one anchor definition. Upstream results include the fundamental tick as the RS time quantum equal to 1 and sector-specific rung selectors that return natural numbers for different particle classes.
proof idea
The proof is a one-line wrapper that unfolds the definition of nu1_spacing and applies norm_num to reduce the expression to the constant 2.
why it matters
This lemma supports the upgraded lightest rung hypothesis in the T14 neutrino sector derivation by supplying the parameter-free 8-tick quarter spacing. It feeds rung_gap_21_is_two to establish the residue difference of 2 between nu2 and nu1, and res_nu1_simp to compute the fractional residue for nu1 as -239/4. It aligns with the eight-tick octave landmark and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.