deep_window_phase_forces_r1_value
plain-language theorem explainer
Under a deep-atmospheric window on the heaviest neutrino rung and the canonical quarter-phase class, every admissible baseline candidate is forced to the lightest-neutrino rung value $-239/4$. Neutrino-sector and absolute-baseline verifiers cite this as the numeric collapse of the choice set. The proof lifts the integer numerator forcing lemma and rewrites through the quarter-rung definition.
Claim. Let $c$ be a baseline candidate parameterized by a quarter-rung numerator for the lightest neutrino rung $r_1(c)=r_{1,\mathrm{num}}(c)/4$. If $c$ lies in the deep atmospheric window and in the canonical $-1/4$ quarter-phase class, then $r_1(c)=(-239)/4$.
background
The module closes a finite-search step for the neutrino absolute baseline. Candidates are encoded by an integer quarter-rung numerator: a BaselineCandidate is just $r_{1,\mathrm{num}}\in\mathbb{Z}$, with $r_1=r_{1,\mathrm{num}}/4$. Structural gaps are imposed in numerator form ($+2$, then $+7/2$), so the heavier rungs $r_2,r_3$ are determined once $r_1$ is fixed.
Two Boolean filters cut the pool: a deep-atmospheric window on $r_3$, and membership in the canonical quarter-phase class (the $-1/4$ phase). The module claim is that these constraints collapse the admissible set to the singleton $r_1=-239/4$.
This declaration states the forced rational value of $r_1$ itself. An upstream sibling forces the integer numerator $r_{1,\mathrm{num}}=-239$ under the same window and phase hypotheses; the present result only packages that numerator into the quarter-rung scale used by the mass ladder.
proof idea
Term-mode, two steps. First apply the numerator forcing lemma deep_window_phase_forces_r1_num to the same candidate and the two Boolean hypotheses, obtaining $c.r_{1,\mathrm{num}}=-239$. Then simp through the definitions of $r_1$ and the quarter-rung map, substituting that numerator equality, which yields $r_1(c)=(-239)/4$.
why it matters
This is the numeric half of the O5 neutrino baseline closure: once the deep window and quarter-phase class are imposed, the lightest rung is pinned exactly at $-239/4$. The immediate parent is deep_window_phase_forces_res_nu1, which rewrites the same conclusion as equality with the canonical baseline residue res_nu1 ("With built-in spacing, the same forcing aligns with the canonical baseline res_nu1").
In the broader RS picture this feeds absolute placement on the $\phi$-ladder mass formula (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), fixing the neutrino sector baseline rather than leaving a free overall shift. It does not itself derive the gap profile or the atmospheric window; those are inputs. Together with the residue alignment theorem it turns the enumerated choice set into a singleton matching the canonical neutrino residues.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.