deepAtmosphericWindow
plain-language theorem explainer
Boolean filter selecting neutrino baseline candidates whose atmospheric rung numerator lies in the open integer window (−220, −216), i.e. rung in (−55, −54). Cited by the admissible-set filter and by the forcing lemmas that pin r3_num = −217 and r1_num = −239. Implemented as a one-line decidable inequality on the quarter-rung numerator.
Claim. For a baseline candidate $c$ (encoded by the quarter-rung numerator of the lightest neutrino), return true iff the atmospheric numerator satisfies $-220 < n_3(c) < -216$, equivalently the atmospheric rung lies in the open interval $(-55,-54)$.
background
The module closes the absolute neutrino baseline by finite search. Candidates are parameterized by an integer quarter-rung numerator for the lightest state: $r_1 = r_{1,\mathrm{num}}/4$. Structural gaps fix the heavier numerators ($r_2-r_1=2$, then a $+7/2$ step to $r_3$), so the atmospheric rung is determined once $r_1$ is chosen.
The deep-atmospheric window is the open interval $(-55,-54)$ on the rung ladder, written in numerator units as $(-220,-216)$. It sits next to the eight-tick phase structure (T7) and the canonical quarter-phase class (atmospheric rung at integer minus $1/4$). The tick and phase infrastructure supply the discrete time/phase lattice on which these rung numerators live; fermion anchor rungs give the reference ladder positions for $\nu_1,\nu_2,\nu_3$.
proof idea
Definition, not a proof. Body is a single decide on the conjunction $-220 < r3_num,c \land r3_num,c < -216$. Decidability of integer order makes the Boolean total and computable for the finite candidate pool.
why it matters
First conjunct of the combined admissibility filter (admissible = deep window ∧ quarter-phase class ∧ structural gap profile). Downstream forcing theorems use it to collapse the search: with the quarter-phase class it forces $r3_num=-217$ and $r3=-217/4$; with fixed spacing it forces $r1_num=-239$ and $r1=-239/4$, the singleton baseline stated in the module doc. Edge-confinement also shows the window is automatic once the atmospheric numerator is fixed at $4\cdot\mathrm{rung}_{\nu_3}-1$. This is the O5 finite-search step that pins the absolute neutrino baseline on the $\varphi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.