quarterPhaseClass
plain-language theorem explainer
Boolean filter on a neutrino baseline candidate that holds exactly when the atmospheric rung sits at integer-minus-one-quarter on the quarter ladder. The finite-search admissibility predicate and the deep-window forcing lemmas cite it to pin the canonical phase class. Body is a one-line modular check on the r3 numerator.
Claim. Given a baseline candidate $c$ with atmospheric rung numerator $r_3^{\mathrm{num}}(c)$, return true iff $(r_3^{\mathrm{num}}(c)+1)\equiv 0\pmod{4}$. Equivalently, the atmospheric rung equals an integer minus $1/4$ on the quarter ladder.
background
The module enumerates neutrino absolute baselines by quarter-rung numerators. A BaselineCandidate is just an integer $r_1^{\mathrm{num}}$ with lightest rung $r_1=r_1^{\mathrm{num}}/4$. Structural spacing fixes $r_2-r_1=2$ and $r_3-r_2=7/2$, so the atmospheric numerator is $r_3^{\mathrm{num}}(c)=r_1^{\mathrm{num}}+22$.
The quarter embedding maps $k\mapsto k/4$ on the rung lattice. The eight-tick octave (forcing chain T7) makes phase classes modulo 4 meaningful: the canonical atmospheric placement is integer minus one quarter. This definition is the Boolean test for that class.
Upstream gap machinery (Gap45 product of closure and Fibonacci factors; RSBridge anchor display $F(Z)$) supplies the broader mass-ladder context, but the check itself is pure modular arithmetic on the candidate's $r_3$ numerator.
proof idea
Definition, not a theorem. Body is decide of the decidable proposition $((r_3^{\mathrm{num}}(c)+1)\bmod 4)=0$ on integers. No lemmas are applied; the equality is evaluated by the integer modular arithmetic instance.
why it matters
Closes the canonical $-1/4$ phase-class half of the O5 neutrino baseline search. Combined with the deep-atmospheric window and structural gap profile inside admissible, it forces the candidate pool to a singleton.
Downstream forcing theorems use it directly: deep-window plus this phase class yield $r_3^{\mathrm{num}}=-217$, $r_1^{\mathrm{num}}=-239$, and the rung values $r_3=-217/4$, $r_1=-239/4$, aligning with the canonical res_nu1. Edge-confinement lemmas also route through it.
Framework landmark: eight-tick octave (T7, period $2^3$), realized here as the quarter-ladder phase condition on the atmospheric rung. Without this filter the baseline set does not collapse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.