quarter_phase_forced_from_eight_tick_offset
plain-language theorem explainer
If a neutrino baseline candidate has third-rung numerator equal to the deepest-edge atmospheric value 4·rung_ν3−1, then it automatically sits in the canonical quarter-phase (−1/4) class. Neutrino-sector baseline enumerators cite this to drop the phase filter as an independent constraint. The proof reduces the atmospheric numerator to −217 and discharges the phase predicate by simplification against the 8-tick modular definition.
Claim. Let $c$ be a baseline candidate parameterized by a quarter-rung numerator. If the third-generation rung numerator of $c$ equals the deepest-edge atmospheric value $4\,\mathrm{rung}_{\nu_3}-1$, then $c$ lies in the quarter-phase class (the canonical $-1/4$ phase under 8-tick modular arithmetic).
background
This module closes a finite-search step for the absolute neutrino baseline. Candidates are encoded by an integer quarter-rung numerator for the lightest state, $r_1=r_{1,\mathrm{num}}/4$. Structural mass gaps are imposed in numerator form ($+2$, then $+7/2$), together with a deep-atmospheric window on $r_3$ and the canonical $-1/4$ phase class. Under those filters the admissible set collapses to the singleton $r_1=-239/4$.
The eight-tick structure supplies discrete phases $k\pi/4$ for $k=0,\ldots,7$ (the T7 octave). The quarter-phase class is the modular condition that selects the $-1/4$ slot in that cycle. The hypothesis here is the edge-confinement atmospheric numerator $r_{3,\mathrm{num}}(c)=4,\mathrm{rung}_{\nu_3}-1$, the same numerical anchor used for the deep-window filter.
proof idea
Two short steps. First, rewrite the hypothesis with deepest_edge_atmospheric_num_eq to obtain the concrete integer identity $r_{3,\mathrm{num}}(c)=-217$. Second, unfold quarterPhaseClass and simplify against that value; the 8-tick modular predicate evaluates to true. No case split or induction is required: the phase class is a pure arithmetic check once the atmospheric numerator is pinned.
why it matters
Feeds directly into filter_pair_forced_from_edge_confinement, which packages the deep-window and quarter-phase filters as a single conjunction forced by the edge-confinement atmospheric numerator. That joint forcing is the last filter pair in the O5 neutrino baseline enumeration: once both flags are automatic, the search reduces to the structural gap profile and the lightest-rung numerator, collapsing to $r_1=-239/4$.
Framework-wise this is an 8-tick (T7) modular consequence inside the neutrino sector, not a new dynamical law. It shows the canonical $-1/4$ phase is not an extra phenomenological knob once deepest-edge atmospheric confinement is accepted. Downstream baseline uniqueness arguments can therefore treat phase class as derived rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.