structuralGapProfile
plain-language theorem explainer
Boolean check that a neutrino baseline candidate obeys the structural rung gaps +2 then +7/2, written in quarter-rung numerators as differences 8 and 14. Cited by the combined admissibility filter that collapses the absolute-baseline search to the singleton r1 = -239/4. The body is a one-line decidable equality on the two numerator differences.
Claim. For a baseline candidate $c$ with lightest-neutrino quarter-rung numerator $r_{1,\mathrm{num}}$, return true iff the derived numerators satisfy $r_{2,\mathrm{num}}-r_{1,\mathrm{num}}=8$ and $r_{3,\mathrm{num}}-r_{2,\mathrm{num}}=14$ (equivalently, rung gaps $r_2-r_1=2$ and $r_3-r_2=7/2$).
background
The module closes a finite-search step for the neutrino absolute baseline. Candidates are parameterized by a single integer, the quarter-rung numerator of the lightest rung: $r_1 = r_{1,\mathrm{num}}/4$. Heavier rungs are then recovered from fixed structural gaps rather than free parameters.
In rung units the profile is $+2$ then $+7/2$. Clearing the quarter denominator converts those gaps into integer numerator differences $8$ and $14$. Sibling definitions supply $r_{2,\mathrm{num}}$ and $r_{3,\mathrm{num}}$ from $r_{1,\mathrm{num}}$ by exactly those offsets, so the predicate is the explicit Boolean form of the gap law used by the search.
The same module later imposes a deep-atmospheric window on $r_3$ and the canonical $-1/4$ phase class. Together the three filters force the admissible set down to the singleton $r_1=-239/4$.
proof idea
Definition, not a proof. The body calls decide on the conjunction of two integer equalities: $r_{2,\mathrm{num}}(c)-c.r_{1,\mathrm{num}}=8$ and $r_{3,\mathrm{num}}(c)-r_{2,\mathrm{num}}(c)=14$. Because the sibling numerator maps are pure arithmetic in $r_{1,\mathrm{num}}$, both sides are closed terms and the decision procedure returns a concrete Bool.
why it matters
This is the structural half of the O5 neutrino baseline choice-set. Downstream, admissible ANDs it with the deep-atmospheric window and the quarter-phase class; the companion theorem structural_gap_profile_holds shows the predicate is identically true once the numerator maps are unfolded, so the gap law is enforced by construction rather than by search.
In the broader RS mass picture, neutrino rungs sit on the $\varphi$-ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Fixing the two successive gaps reduces the three-generation baseline to a single integer, which the remaining filters pin to $-239/4$. The declaration does not itself derive why the gaps are $2$ and $7/2$; it only packages that profile for the finite enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.