deep_window_phase_forces_res_nu3
plain-language theorem explainer
Under the deep-atmospheric window and the canonical quarter-phase class, any neutrino baseline candidate has third rung exactly equal to the canonical atmospheric value −217/4. Neutrino-sector and baseline-enumeration arguments cite this as the r3 half of the collapse to the singleton baseline. The proof is a two-step calc: force the rational value, then match the simplified canonical residual.
Claim. Let $c$ be a neutrino baseline candidate (parameterized by the quarter-rung numerator of the lightest rung). If $c$ lies in the deep atmospheric window and belongs to the canonical quarter-phase class, then its third rung equals the canonical atmospheric residual: $r_3(c)=\mathrm{res}_{\nu_3}=-217/4$.
background
This module closes a finite-search step for the absolute neutrino baseline. Candidates are encoded by an integer quarter-rung numerator for the lightest rung $r_1=r_{1,\mathrm{num}}/4$. The structural gap profile is fixed in numerator form ($+2$, then $+7/2$), so $r_2$ and $r_3$ are determined once $r_1$ is chosen.
Two Boolean filters cut the pool: a deep-atmospheric window on $r_3$, and membership in the canonical $-1/4$ quarter-phase class. The module claim is that these constraints collapse the admissible set to the singleton $r_1=-239/4$.
The present theorem isolates the atmospheric half of that collapse: window plus phase force $r_3$ onto the named canonical residual $\mathrm{res}_{\nu_3}$. Downstream, edge-confinement supplies the same filters and pairs this identity with the matching $r_1$ statement.
proof idea
Two-line calc. First apply deep_window_phase_forces_r3_value to the candidate and the two Boolean hypotheses, obtaining $r_3(c)=(-217:\mathbb{Q})/4$. Then rewrite the right-hand side by simpa against the symmetry of res_nu3_simp, which identifies that rational with the canonical atmospheric residual. No case split or search remains at this layer.
why it matters
Feeds directly into edge_confinement_forces_canonical_baseline, whose doc-comment states the full forcing: filters forced from edge-confinement atmospheric level, then $r_3$ and $r_1$ collapse to canonical $\mathrm{res}{\nu_3}$ and $\mathrm{res}{\nu_1}$. This theorem is the $r_3$ conjunct of that pair.
In the Recognition neutrino sector the absolute baseline is not free: structural gaps, the deep atmospheric window, and the quarter-phase class are meant to pin the phi-ladder rungs. Aligning $r_3$ with $\mathrm{res}_{\nu_3}$ is the atmospheric half of the O5 finite-search closure that reduces the choice set to $r_1=-239/4$.
It does not by itself finish the baseline story; the companion $r_1$ forcing and the edge-confinement filter derivation sit one step downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.