absolute_baseline_num_forced_eq_neg239
plain-language theorem explainer
Under the deep-atmospheric ladder constraint on the heaviest neutrino rung numerator, the lightest-neutrino quarter-rung numerator is forced to equal -239. Neutrino-sector verifiers cite this to pin the absolute baseline at D=3. The proof subtracts the fixed structural gap sum from the deep-ladder value, then evaluates at the known atmospheric rung.
Claim. Let $c$ be a baseline candidate, encoded by the quarter-rung numerator of the lightest neutrino rung $r_1=r_{1,\mathrm{num}}/4$. If the third-rung numerator satisfies $r_{3,\mathrm{num}}(c)=4\,r_{\nu_3}-1$ (deep-atmospheric window), then $r_{1,\mathrm{num}}(c)=-239$.
background
This module closes a finite-search step for the neutrino absolute baseline. Candidates are parameterized by an integer quarter-rung numerator: $r_1=r_{1,\mathrm{num}}/4$. The structural gap profile is imposed in numerator form ($+2$, then $+7/2$), together with a deep-atmospheric window on $r_3$ and the canonical $-1/4$ phase class. Under those constraints the admissible set collapses to the singleton $r_1=-239/4$.
A baseline candidate is just that integer numerator. The deep-ladder hypothesis says the third numerator equals $4,r_{\nu_3}-1$, i.e. $r_3$ sits at the atmospheric window edge. The companion lemma absolute_baseline_num_forced_from_deep_ladder already converts that window into $r_{1,\mathrm{num}}=(4,r_{\nu_3}-1)-22$ by subtracting the fixed gap sum in numerator units. This theorem only evaluates that expression at the concrete atmospheric rung.
proof idea
One calc block. First rewrite $r_{1,\mathrm{num}}$ via the upstream identity that the deep-ladder window forces $r_{1,\mathrm{num}}=(4,r_{\nu_3}-1)-22$. Then close by norm_num after unfolding the concrete integer value of $r_{\nu_3}$, which yields $-239$. No case splits or induction.
why it matters
Feeds the O5' surface theorem: deep-ladder atmospheric confinement is equivalent to the single canonical baseline candidate. That parent applies this result to obtain $r_{1,\mathrm{num}}=-239$, then matches the structure to the canonical field. Together they finish the module's claim that the admissible baseline set is the singleton $r_1=-239/4$.
The doc-comment flags the $D=3$ specialization (forcing-chain T8). In the broader RS mass picture, neutrino rungs sit on the $\varphi$-ladder with yardstick $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$; fixing the absolute baseline numerator removes the remaining discrete freedom in the lightest rung before mass predictions are read off. Closes the numeric half of the O5 progress step in this verification module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.