r2
plain-language theorem explainer
Defines the second neutrino baseline rung as a rational: the candidate's first-rung quarter-numerator plus eight, divided by four. That encodes the fixed structural gap of two full rungs between the lightest and middle neutrino. Anyone enumerating the admissible neutrino baseline set, or citing the O5 finite-search collapse to r1 = -239/4, uses this accessor. The body is a one-line composition of the gap numerator with the quarter-rung converter.
Claim. For a baseline candidate $c$ encoded by an integer quarter-rung numerator $n_1$, the second neutrino rung is the rational $r_2(c) = (n_1 + 8)/4$. Equivalently $r_2 = r_1 + 2$, where $r_1 = n_1/4$, implementing the structural gap $r_2 - r_1 = 2$.
background
The module closes a finite-search step for the absolute neutrino baseline. Candidates are parameterized solely by an integer quarter-rung numerator $n_1$ for the lightest rung $r_1 = n_1/4$. The structural gap profile of the neutrino sector is fixed in numerator form: first gap $+2$ (eight quarter-rungs), then $+7/2$ (fourteen quarter-rungs), together with a deep-atmospheric window on $r_3$ and the canonical $-1/4$ phase class.
quarterRung converts any integer numerator $n$ to the rational rung $n/4$. The sibling numerator for the middle rung is $n_2 = n_1 + 8$, which is exactly the $+2$ gap written in quarter units. Under those constraints the admissible set collapses to the singleton $r_1 = -239/4$.
proof idea
Pure definitional composition, no proof obligations. Apply the structural numerator $n_2 = n_1 + 8$, then convert by quarter-rung division: $r_2 = n_2/4$. Unfolding yields $r_2 = r_1 + 2$ immediately.
why it matters
This accessor is the middle rung in the neutrino baseline triple used by the O5 choice-set enumeration. Downstream, the NeutrinoSector prediction bounds on the lightest fractional mass and the lepton-generation uniqueness/torsion-minimality results sit on the same phi-ladder rung language (charged leptons use the integer triple ${2,13,19}$; neutrinos use the quarter-rung baseline). The gap $+2$ then $+7/2$ is the neutrino-sector counterpart of the charged-lepton step pattern, so the definition keeps the baseline search aligned with the mass-formula yardstick $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. It feeds the candidate pool and the canonical-candidate singleton that discharge the absolute-baseline question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.