Formal proof that a categorical phase-skip detector catches what CUSUM/GLR can't | Heykuki News