valid_candidates_singleton
plain-language theorem explainer
Under the structural gap profile, deep-atmospheric window, and canonical quarter-phase filter, the finite list of admissible neutrino baseline candidates equals exactly the singleton containing the canonical choice (lightest rung numerator $-239$). Anyone citing the O5 baseline collapse or uniqueness of the neutrino absolute rung will use this. The proof is a one-line native decision on the filtered finite pool.
Claim. The filtered list of admissible baseline candidates equals the singleton list whose only element is the canonical candidate with lightest-neutrino quarter-rung numerator $r_{1,\mathrm{num}}=-239$ (equivalently $r_1=-239/4$).
background
The module closes a finite-search step for the neutrino absolute baseline. Baselines are parameterized by a quarter-rung numerator for the lightest neutrino; the structural gap profile is fixed in numerator form as $+2$ then $+7/2$, and $r_3$ is required to lie in a deep-atmospheric window in the canonical $-1/4$ phase class.
A baseline candidate is a record carrying that numerator. The canonical candidate is the concrete record with numerator $-239$. The candidate pool is a finite search window of deep-ladder baselines that contains this value. Admissible candidates are those that survive the gap, window, and phase filters; validCandidates is exactly that filtered list.
The local claim is that, once those filters are imposed, the admissible set collapses to a singleton.
proof idea
One-line wrapper: native_decide evaluates equality of the two concrete lists after the finite filter is applied. No algebraic lemmas are invoked; the decision procedure checks that the filtered pool is definitionally the singleton whose head is the canonical candidate.
why it matters
This is the computational heart of the O5 neutrino baseline choice-set collapse. Downstream, baseline_choice_set_collapsed is a named summary that re-exports the same equality; canonical_is_valid rewrites with it to place the canonical record in the admissible list; unique_valid_candidate rewrites membership to conclude every admissible candidate equals the canonical one.
In the Recognition mass ladder, neutrino rungs sit on the $\varphi$-ladder with the structural gap profile. Pinning the lightest rung numerator to $-239$ (so $r_1=-239/4$) removes residual discrete freedom in the absolute neutrino baseline under the stated filters, which is the enumerated-choice closure the module advertises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.