deepestEdgeOnlyAtmospheric
plain-language theorem explainer
Predicate selecting integer atmospheric numerators that sit in the open deep window (−220, −216) and in the canonical −1/4 phase class (n ≡ −1 mod 4). Neutrino-baseline enumeration cites it to pin the atmospheric rung before collapsing the lightest-neutrino choice set. The body is a pure conjunction of two arithmetic constraints; no proof work.
Claim. An integer $n$ satisfies the deepest edge-only atmospheric condition when $-220 < n < -216$ and $n \equiv -1 \pmod{4}$ (equivalently $(n+1) \bmod 4 = 0$).
background
The module closes a finite-search step for the neutrino absolute baseline. Lightest-neutrino rungs are parameterized by a quarter-rung numerator; structural gaps are fixed in numerator form as $+2$ then $+7/2$; a deep-atmospheric window is imposed on the third rung together with the canonical $-1/4$ phase class. Under those constraints the admissible set collapses to the singleton $r_1 = -239/4$.
This definition packages the two atmospheric-side filters: membership in the open integer interval $(-220,-216)$ (the deep window) and congruence to the $-1/4$ phase class. Downstream uniqueness then reads off a single atmospheric numerator from those filters alone.
proof idea
Definitional abbreviation only: the predicate is the conjunction of the strict window inequalities $-220 < n < -216$ with the modular condition $(n+1)\bmod 4 = 0$. No lemmas are invoked.
why it matters
Feeds the uniqueness theorem deepest_edge_only_forces_atmospheric_num, whose doc-comment states that within the deep window the $-1/4$ phase class picks a unique atmospheric numerator ($n=-217$). That uniqueness is a necessary filter in the O5 neutrino baseline choice-set enumeration: once the atmospheric numerator is forced, the structural gap profile and quarter-rung parameterization collapse the lightest baseline to $r_1=-239/4$. The construction sits in the verification layer that checks RS mass-ladder numerics against the phi-ladder mass formula, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.