r2_num
plain-language theorem explainer
The second neutrino rung numerator is the lightest-rung numerator plus eight, encoding the fixed structural gap of two full rungs in quarter-rung units. Anyone enumerating admissible neutrino baselines under the O5 gap profile cites this encoding. It is a one-line arithmetic definition on the candidate structure.
Claim. For a baseline candidate with lightest-neutrino quarter-rung numerator $n_1\in\mathbb{Z}$, the second-rung numerator is $n_2:=n_1+8$, so that the corresponding quarter-rungs satisfy $r_2-r_1=2=8/4$.
background
The module closes a finite-search step for the neutrino absolute baseline. Candidates are parameterized by a single integer: the quarter-rung numerator of the lightest neutrino, so $r_1=n_1/4$. The structural gap profile then forces the next two rungs by fixed offsets ($+2$, then $+7/2$) written in numerator form.
A baseline candidate is just that integer $n_1$. The second rung is recovered by adding eight to $n_1$, because two full rungs equal eight quarter-rungs. The third rung uses a further offset of fourteen quarter-rungs ($7/2$). Downstream filters impose 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$.
proof idea
Pure definition: return the candidate's lightest-rung numerator plus eight. No lemmas or tactics; the arithmetic is the content. The companion rational $r_2$ is then quarterRung of this integer.
why it matters
This numerator is the bridge from the free parameter $n_1$ to the middle rung of the structural gap profile. It is consumed by the rational $r_2$, by the Boolean structuralGapProfile (which checks $n_2-n_1=8$ and $n_3-n_2=14$), and by the theorem that the profile holds identically for every candidate. Together with the atmospheric window and phase class, those filters discharge the O5 enumeration that pins the lightest neutrino at $r_1=-239/4$. In the broader RS mass ladder the same quarter-rung bookkeeping sits under the phi-ladder mass formula; here it is specialized to the three-neutrino baseline search.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.