structural_gap_profile_holds
plain-language theorem explainer
Every neutrino baseline candidate, coded by an integer quarter-rung numerator for the lightest species, automatically satisfies the structural gap profile of successive spacings +2 then +7/2. Sector verifiers use this when the finite choice set is filtered down to the singleton r1 = -239/4. The proof is a one-line simplification: the second and third numerators are defined so the profile holds identically.
Claim. For every baseline candidate $c$ (an integer quarter-rung numerator with $r_1 = r_{1,\mathrm{num}}/4$), the structural gap profile evaluates to true: the successive rung gaps are $r_2-r_1=+2$ and $r_3-r_2=+7/2$ (equivalently numerator shifts $+8$ then $+14$).
background
Recognition Science places neutrino masses on the phi-ladder via a yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. Absolute placement of the lightest rung is still open; this module treats it as a finite-search problem. A baseline candidate is only an integer $r_{1,\mathrm{num}}$ with $r_1=r_{1,\mathrm{num}}/4$.
The local filters are: (i) a structural gap profile $+2$ then $+7/2$ between the three neutrino rungs, (ii) a deep-atmospheric window on $r_3$, and (iii) the canonical $-1/4$ phase class. Under all three, the admissible set collapses to the singleton $r_1=-239/4$. The atmospheric numerator comment records the deepest-edge construction $4\cdot(-54)-1=-217$ from $\mathrm{rung}_{\nu_3}=-54$ with quarter-phase offset.
Here the second and third numerators are defined from $r_{1,\mathrm{num}}$ by those fixed gaps ($r_{2,\mathrm{num}}=r_{1,\mathrm{num}}+8$, and the matching $+14$ step to $r_{3,\mathrm{num}}$), so the profile is part of the candidate encoding rather than an external constraint.
proof idea
One-line simp proof. Unfolding the structural-gap-profile predicate together with the definitions of the second and third rung numerators reduces the goal to a Boolean identity. Those numerators are defined exactly so the gaps $+2$ and $+7/2$ hold for every integer lightest-rung numerator; no external lemmas are invoked. The claim is definitional once the candidate type is fixed.
why it matters
This discharges the gap-profile filter for free on the whole candidate type, so the O5 neutrino baseline enumeration only still has to check the deep-atmospheric window and the canonical $-1/4$ phase class. That is the finite-search closure step described in the module: under those constraints the admissible set is the singleton $r_1=-239/4$.
Relative skeleton first, absolute placement second, matches the RS mass-formula workflow on the phi-ladder. The quarter-phase class ties to the eight-tick octave (T7) phase grid $k\pi/4$. No downstream users are recorded yet; the theorem is local infrastructure for the choice-set singleton argument inside this verification module. It does not itself derive the $+2$ and $+7/2$ gaps from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.