valid_candidate_count
plain-language theorem explainer
Under the neutrino baseline constraints (quarter-rung lightest mass, structural gaps +2 then +7/2, deep-atmospheric window, canonical −1/4 phase), the admissible candidate list has length exactly one. Neutrino-sector uniqueness arguments cite this as the finite-search closure that pins r1 = −239/4. The proof is a one-line native_decide on the filtered pool.
Claim. The filtered list of admissible neutrino baseline candidates has length $1$: exactly one triple of quarter-rung numerators survives the structural gap profile, the deep-atmospheric window on the heaviest rung, and the canonical $-1/4$ phase class.
background
The module closes a finite-search step for the absolute neutrino baseline in Recognition Science. The lightest neutrino rung is parameterized by a quarter-rung numerator; the other two rungs are forced by the structural gap profile written in numerator form as successive offsets $+2$ and $+7/2$. A deep-atmospheric window is imposed on the heaviest rung together with the canonical $-1/4$ phase class.
Admissible candidates are obtained by filtering a finite candidatePool with those predicates. The module claim is that this filter collapses the choice set to the singleton baseline $r_1 = -239/4$.
List length here is ordinary finite-list cardinality (the same length primitive used for finite traces elsewhere in the foundation).
proof idea
One-line wrapper: native_decide evaluates the concrete filtered list validCandidates (the candidate pool restricted by the admissibility predicate) and checks that its length equals 1. No algebraic lemma is invoked; the result is pure computational discharge of a closed finite enumeration.
why it matters
This is the O5 progress marker for neutrino absolute-baseline uniqueness: once the structural gap profile, deep-atmospheric window, and canonical phase class are fixed, the admissible set is a singleton rather than an open family. Downstream neutrino-sector mass formulas can therefore treat $r_1 = -239/4$ as the forced lightest rung instead of a free parameter.
In the broader RS ladder picture, neutrino masses sit on the same $\varphi$-rung yardstick as the charged fermions; pinning the baseline removes the last discrete ambiguity in that sector. No parent theorem currently consumes the count (used-by is empty), so the result stands as a self-contained verification lemma ready for uniqueness corollaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.