deep_window_phase_forces_r3_value
plain-language theorem explainer
Under the deep atmospheric window and canonical quarter-phase filters, the atmospheric neutrino rung is forced to exactly $-217/4$. Anyone closing the finite neutrino baseline choice set cites this uniqueness step. The proof reduces the rational claim to the integer-numerator forcing lemma and unfolds the quarter-rung definition.
Claim. For any baseline candidate $c$ (parameterized by the lightest-neutrino quarter-rung numerator), if the atmospheric rung lies in the open window $(-55,-54)$ and belongs to the canonical quarter-phase class (atmospheric value congruent to $-1/4$ modulo $1$), then that atmospheric rung equals $-217/4$.
background
This module closes a finite-search step for the neutrino absolute baseline. Candidates are encoded by a single integer numerator $r_{1,\mathrm{num}}$ with $r_1 = r_{1,\mathrm{num}}/4$. Structural gaps fix the higher rungs in numerator form: $r_2 - r_1 = 2$ and the atmospheric gap that determines $r_3$.
The deep atmospheric window requires the atmospheric numerator in $(-220,-216)$, i.e. the rung in $(-55,-54)$. The quarter-phase class is the canonical 8-tick condition that the atmospheric rung sits at an integer minus $1/4$. Together these filters are the local selection rules for admissible baselines.
Upstream, an integer lemma already forces the atmospheric numerator to $-217$ under the same two Boolean filters. The present statement lifts that integer uniqueness to the rational rung value used downstream.
proof idea
Term-mode, two steps. First apply the sibling lemma deep_window_phase_forces_r3_num to the same candidate and hypotheses, obtaining $r_{3,\mathrm{num}}(c) = -217$. Then simplify the definition of the atmospheric rung $r_3$ (via the quarter-rung constructor) against that equality, yielding $r_3(c) = -217/4$. No case split or arithmetic search remains at this layer.
why it matters
This is the rational-value form of atmospheric-rung uniqueness inside the O5 neutrino baseline enumeration. The immediate parent is deep_window_phase_forces_res_nu3, which rewrites the same conclusion as equality with the canonical atmospheric residue res_nu3, aligning the choice-set filter with the named neutrino sector constant.
In the broader Recognition ladder, neutrino masses sit on the $\varphi$-rung yardstick; fixing $r_3 = -217/4$ under the deep window and 8-tick phase class is a concrete step toward collapsing the admissible baseline set to the singleton $r_1 = -239/4$ announced in the module header. It does not itself derive the gap profile or the window bounds; it converts those filters into a unique atmospheric rung value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.