r1
plain-language theorem explainer
Maps a neutrino baseline candidate to the lightest-neutrino rung as a rational: the candidate's integer quarter-rung numerator divided by four. Anyone working the absolute neutrino baseline or the O5 finite-search closure cites it as the decoded r1 coordinate. The body is a one-line application of the quarter-rung converter.
Claim. For a baseline candidate $c$ encoded by an integer quarter-rung numerator $n$, the lightest neutrino rung is the rational $r_1(c) = n/4$.
background
The module closes a finite-search step for the absolute neutrino baseline. Candidates are parameterized by a single integer numerator for the lightest rung; the structural gap profile is then imposed in numerator form ($+2$, then $+7/2$), together with a deep-atmospheric window on $r_3$ and the canonical $-1/4$ phase class. Under those constraints the admissible set collapses to the singleton $r_1 = -239/4$.
A BaselineCandidate is just that integer numerator $n$ for $r_1 = n/4$. The helper quarterRung converts any such numerator to a rational by dividing by four. The present definition is the decoded $r_1$ coordinate of a candidate: apply that conversion to the candidate's numerator. Rungs sit on the $\varphi$-ladder used for mass predictions (yardstick times $\varphi$ to a rung offset).
proof idea
Pure definition, no proof obligations. The body is the one-line term quarterRung c.r1_num, i.e. cast the candidate numerator to $\mathbb{Q}$ and divide by $4$.
why it matters
This is the decoded lightest-neutrino rung used throughout the baseline choice-set enumeration. Downstream neutrino-sector bounds (e.g. fractional predictions for $\nu_1$) read $r_1$ off candidates before checking the deep-atmospheric window and phase class. The module goal is the O5 collapse to the singleton $r_1 = -239/4$; without a uniform rational decoder the finite search cannot state uniqueness. In the broader RS mass ladder, neutrino rungs feed the same $\varphi$-power mass formula as charged leptons, so a fixed baseline anchors absolute scale comparisons once the gap profile is enforced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.