baseline_choice_set_collapsed
plain-language theorem explainer
Under the O5 neutrino baseline filters (quarter-rung numerators, structural gap profile +2 then +7/2, deep-atmospheric window on r3, and the canonical −1/4 phase class), the admissible baseline list equals the singleton containing the canonical candidate r1 = −239/4. Anyone citing the finite-search closure of the absolute neutrino baseline would use this. The proof is a one-line term that names the already-proved singleton lemma.
Claim. The filtered list of admissible neutrino baseline candidates equals the singleton list whose only entry is the canonical candidate (lightest rung $r_1 = -239/4$).
background
This module closes a finite-search step for the neutrino absolute baseline (O5). The lightest neutrino rung is parameterized by a quarter-rung numerator; the other two rungs are then fixed by the structural gap profile written in numerator form as successive offsets $+2$ and $+7/2$. Two further filters are imposed: a deep-atmospheric window on the heaviest rung $r_3$, and membership in the canonical $-1/4$ phase class.
The objects in play are the candidate pool of quarter-rung baselines, the structural gap profile, the deep-atmospheric window, and the quarter-phase class. The canonical candidate is the unique pool member that survives all of those filters, with $r_1 = -239/4$. The claim asserts that the filtered list of valid candidates is exactly that singleton.
Recognition Science places neutrino masses on the $\phi$-ladder (mass yardstick times $\phi$ to a rung offset). The baseline choice fixes the absolute zero of that ladder for the neutrino sector; collapsing the choice set removes residual discrete ambiguity before mass predictions are read off.
proof idea
One-line term proof: the equality is definitionally the already-established lemma that the valid-candidate list is a singleton consisting of the canonical candidate. No extra tactics or algebraic work occur at this declaration; it is a named summary alias for that singleton result under the current filter set.
why it matters
In the Recognition framework the neutrino sector sits on the $\phi$-ladder with absolute baseline still under discrete search (O5). This theorem records the enumerated-choice closure: after the structural gap profile, deep-atmospheric window, and canonical phase class are imposed, only one baseline remains ($r_1 = -239/4$). Downstream mass and mixing predictions can therefore treat the absolute rung zero as fixed rather than as a residual choice.
No further used-by edges are recorded yet; the declaration is the module-level summary of the collapse. It does not itself derive the gap profile or the atmospheric window; it packages their joint filtering outcome. Together with the mass formula (yardstick $\cdot \phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) it pins the neutrino absolute scale once those upstream filters are accepted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.