unique_valid_candidate
plain-language theorem explainer
Any admissible neutrino baseline candidate equals the canonical one with quarter-rung numerator -239 (so r1 = -239/4). Verification authors cite this when collapsing the finite search over lightest-neutrino rungs to a singleton under structural gaps, atmospheric window, and phase class. The proof rewrites membership through the already-proved singleton lemma on the admissible list and simplifies.
Claim. Let $c$ be a baseline candidate, encoded by an integer quarter-rung numerator so that the lightest-neutrino rung is $r_1 = r_{1,\mathrm{num}}/4$. If $c$ belongs to the finite list of admissible candidates (structural gap profile, deep-atmospheric window, and canonical $-1/4$ phase class), then $c$ equals the canonical candidate with numerator $-239$.
background
The Neutrino Baseline Choice-Set Enumeration module closes a finite-search step for the absolute neutrino baseline. The lightest neutrino rung is parameterized by a quarter-rung numerator $r_{1,\mathrm{num}}$, giving $r_1 = r_{1,\mathrm{num}}/4$. Structural gaps are imposed in numerator form ($+2$, then $+7/2$), together with a deep-atmospheric window on $r_3$ and the canonical $-1/4$ phase class.
A baseline candidate is the structure carrying only that integer numerator. The canonical candidate is the one with $r_{1,\mathrm{num}} = -239$. Valid candidates are the members of a finite search pool that pass the admissibility filter. Under the module constraints, the admissible set is asserted to collapse to the singleton $r_1 = -239/4$.
Upstream, the neutrino-sector anchor table records provisional integer rungs for $\nu_1,\nu_2,\nu_3$; this module replaces the free $\nu_1$ choice by an enumerated, constrained search.
proof idea
Short tactic proof. Rewrite the membership hypothesis with the already-established singleton identity for the admissible list (that list equals the singleton containing only the canonical candidate). Then simpa turns membership in that singleton into equality with the canonical candidate. No further case analysis or arithmetic is needed at this step.
why it matters
Parent theorem: any admissible baseline reproduces the current residual rung for $\nu_1$. Uniqueness reduces that claim to a single check on the canonical candidate, via a one-line application of this result followed by the canonical matching lemma.
In the Recognition framework this is the O5 finite-search closure for the neutrino absolute baseline on the $\phi$-ladder (mass formula: yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). It pins the lightest neutrino at $r_1 = -239/4$ once structural gaps, atmospheric window, and phase class are fixed, so downstream neutrino-sector verification no longer carries a free baseline parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.