absolute_baseline_num_forced_from_deep_ladder
plain-language theorem explainer
Under deep-ladder atmospheric confinement of the heaviest neutrino rung, the absolute baseline quarter-rung numerator equals that confined value minus the fixed structural spacing 22. Anyone closing the neutrino baseline choice set cites this reduction. The proof rewrites the structural gap identity and finishes by integer arithmetic.
Claim. For any baseline candidate whose third-rung numerator equals $4 r_{\nu_3}-1$ (deep atmospheric confinement), the first-rung numerator satisfies $r_{1,\mathrm{num}}=(4 r_{\nu_3}-1)-22$.
background
This module closes the neutrino absolute-baseline question by finite search. Candidates are encoded by an integer quarter-rung numerator $r_{1,\mathrm{num}}$ with lightest rung $r_1=r_{1,\mathrm{num}}/4$. The structural gap profile ($+2$, then $+7/2$) becomes, in numerator units, the fixed spacing $r_{3,\mathrm{num}}=r_{1,\mathrm{num}}+22$.
Deep-atmospheric confinement pins the heaviest rung numerator to $4,r_{\nu_3}-1$, the deep-ladder window. Ambient spatial dimension is $D=3$ from the forcing chain (T8). The module then imposes the canonical $-1/4$ phase class and shows the admissible set collapses to the singleton $r_1=-239/4$.
proof idea
Unfold the definition of the third-rung numerator on the deep-ladder hypothesis to obtain $r_{1,\mathrm{num}}+22=4 r_{\nu_3}-1$. Integer linear arithmetic (omega) subtracts 22 and yields the claim. No external lemmas beyond the in-module numerator definition.
why it matters
Immediate parent is the numeric specialization that concludes $r_{1,\mathrm{num}}=-239$ at $D=3$, completing the singleton collapse of the neutrino baseline choice set (O5 progress in the module header). This declaration is the algebraic half of that closure: deep-ladder confinement plus fixed structural spacing force the baseline numerator before the concrete rung value is substituted. It sits in the verification layer that turns the phi-ladder mass formula and neutrino-sector rung assignments into a finite, checkable baseline set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.