deep_window_forced_from_edge_confinement
plain-language theorem explainer
Once the atmospheric rung numerator is fixed by edge confinement to 4·rung_ν₃−1, the deep-atmospheric window filter on a neutrino baseline candidate evaluates to true. Neutrino-sector baseline enumerators cite this to discharge the deep-window half of the O5 choice-set collapse. The proof reduces the confinement identity to the concrete numerator −217 and unfolds the window predicate.
Claim. Let $c$ be a neutrino baseline candidate (parameterized by the quarter-rung numerator of the lightest rung $r_1$). If the atmospheric numerator satisfies $r_3^{\mathrm{num}}(c)=4\,r_{\nu_3}-1$, then the deep-atmospheric window predicate holds for $c$.
background
The module closes a finite-search step for the absolute neutrino baseline in Recognition Science. 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 then a $+7/2$ step to $r_3$, so the whole ladder is determined by the lightest rung.
The deep-atmospheric window is a Boolean filter on that ladder: it accepts only candidates whose atmospheric numerator $r_3^{\mathrm{num}}$ sits at the deepest edge value. Edge confinement supplies the identity $4 r_{\nu_3}-1=-217$ (via deepest_edge_atmospheric_num_eq), tying the RS rung of $\nu_3$ to that concrete integer. The eight-tick octave and quarter-phase class appear as sibling filters in the same enumeration; together they collapse the admissible set to the singleton $r_1=-239/4$.
proof idea
Two short tactic steps. First, rewrite the hypothesis $r_3^{\mathrm{num}}(c)=4 r_{\nu_3}-1$ through the edge-confinement identity deepest_edge_atmospheric_num_eq, obtaining the concrete equality $r_3^{\mathrm{num}}(c)=-217$. Second, unfold the definition of the deep-atmospheric window predicate and simplify with that equality; the predicate is exactly the check $r_3^{\mathrm{num}}=-217$, so the goal reduces to true.
why it matters
This lemma is the deep-window half of the joint filter theorem filter_pair_forced_from_edge_confinement, which states that edge confinement forces both the deep-atmospheric window and the canonical quarter-phase ($-1/4$) class at once. That joint result is the gate that collapses the neutrino baseline choice set to the singleton $r_1=-239/4$ under the structural gap profile ($+2$, then $+7/2$).
In the broader RS ladder, neutrino masses sit on the $\varphi$-rung formula with the eight-tick octave (T7) supplying the modular arithmetic for phase class. Edge confinement of the atmospheric rung is the geometric input; this declaration converts that input into a Boolean filter discharge, so the O5 enumeration can finish without an open search over deep-window candidates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.