candidatePool
plain-language theorem explainer
Finite list of 121 deep-ladder neutrino baseline candidates, with quarter-rung numerators running from -300 through -180. Anyone checking the O5 absolute-baseline enumeration cites it as the raw search window that still contains the canonical value. The body is a one-line map of List.range 121 onto BaselineCandidate records.
Claim. The candidate pool is the finite list of baseline candidates whose quarter-rung numerators are $\{-300,-299,\ldots,-180\}$, i.e. $r_1 = r_{1,\mathrm{num}}/4$ with $r_{1,\mathrm{num}}$ in that integer window.
background
The module closes the neutrino absolute-baseline question by a finite search. Each candidate is a BaselineCandidate: a single integer numerator $r_{1,\mathrm{num}}$ encoding the lightest-neutrino rung as $r_1 = r_{1,\mathrm{num}}/4$. Structural gaps then fix $r_2$ and $r_3$ in numerator form ($+2$, then $+7/2$), and a deep-atmospheric window plus the canonical $-1/4$ phase class are imposed on $r_3$.
Upstream rung data (RSBridge anchors for $\nu_1,\nu_2,\nu_3$ and related fermion rungs) supply the ladder language; the mass formula itself is the usual yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. The present definition only builds the raw finite window that is later filtered.
proof idea
Pure definition, no proof obligations. List.range 121 yields $n = 0,\ldots,120$; each $n$ is sent to the structure with $r_{1,\mathrm{num}} = n - 300$, producing the closed integer interval $[-300,-180]$. Downstream candidate_pool_count discharges length 121 by native_decide; validCandidates is the filter of this list by the admissibility predicate.
why it matters
This is the O5 finite-search closure step for the neutrino absolute baseline. Filtering the pool under the structural gap profile, deep-atmospheric window $(-55,-54)$, and canonical $-1/4$ phase class collapses the admissible set to the singleton $r_1 = -239/4$. Downstream validCandidates and candidate_pool_count consume it directly. In the broader RS ladder (phi-ladder masses, eight-tick octave, T6/T7 landmarks) it pins the lightest-neutrino rung inside a machine-checkable window rather than an open real parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.