res_nu1
plain-language theorem explainer
The declaration defines the rung for the lightest neutrino mass eigenstate ν1 as exactly two rungs below the solar-scale rung ν2. Neutrino mass phenomenologists and Recognition Science modelers cite it when constructing fractional mass predictions or Δm² intervals for the three-generation ladder. The definition is a direct subtraction that inherits the quarter-cycle spacing from the eight-tick structure without additional lemmas.
Claim. Let $r_2$ be the rung assigned to the second neutrino mass eigenstate. The rung for the lightest eigenstate satisfies $r_1 := r_2 - 2$, where the subtracted spacing equals one quarter of the eight-tick cycle.
background
The NeutrinoSector module places neutrinos on the deep φ-ladder at even integer rungs far below the electron rung $R_e=2$. The type Rung is an abbreviation for rational numbers, permitting both integer and fractional positions on the ladder. Masses are obtained by scaling the structural mass by φ raised to the rung power, followed by a display conversion from MeV to eV that reuses the electron structural mass as a calibration anchor.
proof idea
This is a one-line definition that subtracts the canonical lightest rung spacing (defined as 8/4 = 2) from the solar rung res_nu2. No tactics or upstream lemmas beyond the arithmetic on the Rung type are required.
why it matters
The definition supplies the rung value used in NeutrinoMassScaleScoreCardCert and the row_nu1_frac theorem that bounds the fractional mass prediction for ν1. It completes the three-generation ladder inside T14 by enforcing the 8-tick quarter spacing, ensuring the derived Δm²21 and Δm²31 intervals remain consistent with NuFIT bands. The construction directly implements the eight-tick octave (T7) from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.