deepLadderForcedCandidate
plain-language theorem explainer
Deep-ladder atmospheric geometry fixes one baseline candidate for the lightest neutrino by setting its quarter-rung numerator to four times the third-neutrino rung minus twenty-three. Citation target for anyone closing the absolute neutrino baseline under the structural gap profile. The body is a one-field structure instance, not a proved equality.
Claim. The baseline candidate forced by deep-ladder atmospheric geometry is the unique $r_1$ candidate whose quarter-rung numerator equals $r_{1,\mathrm{num}}=(4\,r_{\nu_3}-1)-22$, i.e. the candidate satisfying $r_{3,\mathrm{num}}=4\,r_{\nu_3}-1$ together with the fixed structural spacing $r_{3,\mathrm{num}}=r_{1,\mathrm{num}}+22$ (so $r_1=r_{1,\mathrm{num}}/4$).
background
The module enumerates a finite choice set for the absolute neutrino baseline. Each candidate is a single integer numerator $r_{1,\mathrm{num}}$ encoding the lightest rung as $r_1=r_{1,\mathrm{num}}/4$. Structural gaps are imposed in numerator form: $r_2-r_1=2$ and then a $+7/2$ step, which together give a fixed numerator offset of $22$ between $r_3$ and $r_1$.
A deep-atmospheric window further constrains the heaviest rung $r_3$, and the canonical $-1/4$ phase class is required. Under those filters the admissible set collapses to the singleton $r_1=-239/4$. The third-neutrino rung $r_{\nu_3}$ is imported from the neutrino sector and supplies the absolute atmospheric scale that the deep-ladder window locks onto.
Upstream "canonical" objects in the foundation (arithmetic, dyadic protocols, trace closure, cost projector) fix the ambient Recognition calculus; this definition only packages the geometry-forced numerator inside that setting.
proof idea
Pure structure instance. The single field $r_{1,\mathrm{num}}$ is set to $(4,r_{\nu_3}-1)-22$: the deep-ladder atmospheric numerator $4,r_{\nu_3}-1$ minus the fixed structural spacing $22$. No tactics, no lemmas, no proof obligations beyond inhabiting BaselineCandidate.
why it matters
Feeds two immediate parent results in the same module. First, deep_ladder_forced_candidate_eq_canonical shows by simplification on $r_{\nu_3}$ that this geometry-forced point is definitionally the canonical candidate. Second, deep_ladder_geometry_forces_canonical_baseline recovers the canonical residues $r_3=\mathrm{res}{\nu_3}$ and $r_1=\mathrm{res}{\nu_1}$ from the deep-ladder numerator alone, with no extra pool filters.
That pair is the O5 finite-search closure step: deep atmospheric geometry plus the structural gap profile already pin the absolute baseline, so the admissible set is a singleton rather than an open family. In the broader RS ladder picture this is the neutrino-sector instance of the mass formula (yardstick times $\varphi$ to a rung offset), with the quarter-rung phase class matching the eight-tick octave bookkeeping. It does not itself force $D=3$ or $\varphi$, but it consumes those landmarks once the rung scale is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.