validCandidates
plain-language theorem explainer
Finite list of admissible neutrino absolute-baseline candidates: every quarter-rung numerator from the candidate pool that passes the structural-gap, deep-atmospheric, and canonical −1/4 phase filters. Downstream uniqueness and collapse theorems cite this list as the enumerated choice set. The body is a one-line filter of the pool by the admissibility predicate.
Claim. Let $\mathcal{P}$ be the finite pool of baseline candidates, each encoded by an integer quarter-rung numerator $r_{1,\mathrm{num}}$ with $r_1 = r_{1,\mathrm{num}}/4$. Define $\mathrm{Valid}$ as the sublist of $\mathcal{P}$ consisting of those candidates that satisfy the admissibility predicate (structural gaps $r_2-r_1=2$ and $r_3-r_2=7/2$, deep-atmospheric window on $r_3$, and canonical $-1/4$ phase class).
background
The module closes the neutrino absolute-baseline question by finite search. A baseline candidate is a single integer $r_{1,\mathrm{num}}$; the lightest-neutrino rung is the quarter-rung $r_1 = r_{1,\mathrm{num}}/4$. Sibling numerators fix the structural gap profile in numerator form: $r_2-r_1 = 2$ (i.e. $+8/4$) and then $+7/2$ to $r_3$.
Admissibility further requires $r_3$ to lie in a deep-atmospheric window and the candidate to sit in the canonical $-1/4$ phase class (tied to the eight-tick phase lattice $k\pi/4$). The candidate pool is the finite discrete set over which these filters run. Under the full filter set the admissible list is intended to collapse to the singleton $r_1 = -239/4$.
Local setting is O5 progress in the Verification layer: enumerate, filter, then prove the surviving choice set is a singleton matching the neutrino-sector baseline rung.
proof idea
Pure definition: validCandidates is the list comprehension that retains only those elements of candidatePool for which the Boolean predicate admissible holds. No lemmas are applied; the mathematical content lives in the definitions of the pool and of admissibility (structural gaps, deep-atmospheric window, quarter-phase class). Downstream theorems discharge properties of this list by native_decide or by rewriting through the proved singleton equality.
why it matters
This list is the enumerated object that O5 must collapse. Parent results in the same module use it directly: valid_candidates_singleton and baseline_choice_set_collapsed assert equality with [canonicalCandidate]; valid_candidate_count asserts length one; unique_valid_candidate and canonical_is_valid turn membership into uniqueness; admissible_baselines_match_res_nu1 shows every survivor reproduces the neutrino-module rung res_nu1.
In the broader RS picture the absolute neutrino baseline sits on the $\phi$-ladder mass formula (yardstick times $\phi$ to a rung offset). Fixing $r_1 = -239/4$ by finite admissible search removes a free parameter that would otherwise float relative to the eight-tick octave and the structural gap profile. The declaration itself is only the filtered set; the scientific claim is the collapse proved downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.