deepest_edge_atmospheric_num_eq
plain-language theorem explainer
The atmospheric numerator fixed by deepest-edge confinement equals −217: four times the heaviest-neutrino rung (−54) minus the quarter-phase offset. Anyone closing the neutrino baseline choice set cites this identity. The proof is a one-line numerical evaluation after unfolding the rung definition.
Claim. With the heaviest neutrino rung fixed at $-54$ on the $\varphi$-ladder, the structural atmospheric numerator satisfies $4\cdot(-54)-1=-217$ in $\mathbb{Z}$.
background
The module enumerates admissible absolute baselines for the neutrino sector under Recognition Science constraints. Lightest-neutrino position is parameterized by a quarter-rung numerator; structural gaps ($+2$, then $+7/2$) and a deep-atmospheric window on the heaviest rung, together with the canonical $-1/4$ phase class, are imposed so the admissible set collapses to a singleton.
In the neutrino sector the heaviest rung is the integer constant $-54$. The atmospheric numerator is the integer $4\cdot r-1$ obtained by clearing the quarter-phase denominator: deepest edge level times four, offset by the $-1/4$ phase. That combination is the filter input for both the deep-window predicate and the quarter-phase class check.
Upstream, the rung value is a fixed definition in the neutrino sector module; the edge-confinement language comes from the seven-gaps / posting-layer geometry, but this declaration only needs the numerical rung.
proof idea
Term-mode proof by norm_num after unfolding the heaviest-neutrino rung definition $-54$. Arithmetic is $4\cdot(-54)-1=-216-1=-217$; no lemmas beyond the definition are required.
why it matters
This identity is the numerical bridge from edge confinement to the two forcing filters that shrink the baseline choice set. Downstream, deep_window_forced_from_edge_confinement rewrites any candidate whose atmospheric numerator equals $4\cdot(\text{rung}_{\nu_3})-1$ into the concrete window predicate at $-217$. Likewise quarter_phase_forced_from_eight_tick_offset uses the same rewrite and eight-tick modular arithmetic to force the $-1/4$ phase class.
Together those filters implement the module's O5 closure step: under structural gaps, deep window, and quarter-phase class, the admissible baseline collapses to $r_1=-239/4$. The eight-tick octave (T7) supplies the modular offset that makes the quarter-phase class well-defined; the $\varphi$-ladder mass formula supplies the rung language. The declaration itself is pure arithmetic bookkeeping, but without it the two forcing theorems cannot discharge their hypotheses by simpa.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.