r3_num
plain-language theorem explainer
The atmospheric neutrino rung numerator equals the lightest-neutrino quarter-rung numerator plus 22, encoding the fixed structural gaps +2 then +7/2 on the quarter ladder. Neutrino baseline enumeration cites this when mapping a candidate to its deep-atmospheric rung. The body is a one-line integer shift from the candidate field.
Claim. Given a baseline candidate with lightest-neutrino quarter-rung numerator $n\in\mathbb{Z}$ (so $r_1=n/4$), the atmospheric rung numerator is $n+22$. This is the cumulative quarter-ladder shift from the structural gaps $r_2-r_1=2$ ($=8/4$) and $r_3-r_2=7/2$ ($=14/4$).
background
This module closes the neutrino absolute-baseline question by a finite search. Candidates are parameterized by a single integer: the quarter-rung numerator of the lightest neutrino, so $r_1=r_{1,\mathrm{num}}/4$. The structural gap profile is fixed in numerator form: first $+2$ ($=8/4$) to the middle rung, then $+7/2$ ($=14/4$) to the atmospheric rung.
The quarter-ladder embedding sends an integer $k$ to the rational rung $k/4$. Adding the two gaps gives a total numerator offset of $8+14=22$, so the atmospheric numerator is completely determined by the lightest-neutrino numerator. Downstream constraints then place that atmospheric numerator in a deep window near the charged-lepton anchor scale and force the canonical $-1/4$ phase class.
proof idea
Pure definition: return the candidate's lightest-neutrino quarter-rung numerator plus the constant $22$. No lemmas or tactics; the offset is the sum of the structural numerator gaps $8$ (from $+2$) and $14$ (from $+7/2$).
why it matters
This shift is the arithmetic spine of the O5 baseline collapse. Every deep-ladder forcing theorem rewrites through it: absolute baseline from deep-ladder confinement is $r_{1,\mathrm{num}}=(4,r_{\nu_3}-1)-22$, and the numeric form at $D=3$ yields $r_{1,\mathrm{num}}=-239$. The deep-atmospheric window predicate is stated directly on this numerator, and the iff linking deep-ladder confinement to the singleton canonical candidate uses the same identity.
It therefore turns the structural gap profile into a rigid map from lightest to atmospheric rung, so the admissible set collapses to $r_1=-239/4$ once the deep window and phase class are imposed. That singleton is the verification target for matching the residual atmospheric rung to the RS neutrino sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.