res_nu2
plain-language theorem explainer
The definition sets the solar neutrino rung to the atmospheric rung minus a 3.5-unit spacing. Recognition Science neutrino models cite it to enforce the phi^7 squared-mass ratio between the two scales. It is realized as a direct subtraction that encodes the upgraded quarter-cycle spacing drawn from the eight-tick octave.
Claim. Let $r_3$ be the rung for the atmospheric neutrino mass scale. Define the solar rung by $r_2 := r_3 - 7/2$. This enforces the structural squared-mass ratio $(phi^{r_3}/phi^{r_2})^2 = phi^7$.
background
The NeutrinoSector module derives neutrino masses from the phi-ladder in Recognition Science, placing them on deep negative rungs far below the electron at rung 2. Mass 3 sits near rung -54 and mass 2 near -58 in the structural mass formula (yardstick times phi to the rung power). The module notes a residue difference of 4 between generations that suggests a quarter-ladder period, yet this definition upgrades the spacing to 7/2 for tighter alignment with observed squared-mass ratios. Upstream, the rung is introduced as a natural number in Compat.Constants and the tick is fixed as the fundamental time quantum in Constants, anchoring the eight-tick octave.
proof idea
This is a one-line definition that subtracts the canonical spacing from the atmospheric neutrino rung. The spacing value itself is chosen to realize the 7/2 difference required by the solar scale hypothesis.
why it matters
It supplies the solar rung to the NeutrinoMassScaleScoreCardCert structure that certifies fractional mass predictions against NuFIT bounds and to the dm2_21_frac_pred definition that computes the solar mass-squared difference. The definition completes the T14 neutrino sector step by enforcing the phi^7 ratio that follows from the self-similar phi fixed point (T6) and the eight-tick octave (T7) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.