Function design_phase_plan 

pub fn design_phase_plan(it: &Intersection) -> Option<PhasePlan>

Design the minimal-phase conflict-free plan for an intersection, or None if it has no movements.

The chromatic number χ is pinned between two checkable combinatorial certificates before the SAT solver is ever consulted:

• a maximal clique of mutually-conflicting movements proves χ ≥ |clique| (you can verify it by eye — every pair really is in conflict), and
• a greedy proper colouring is a self-checking witness that χ ≤ greedy.

When those meet (|clique| == greedy) the greedy colouring is provably optimal and we return it with zero SAT calls — the common case for the perfect-ish conflict graphs real intersections produce. Otherwise we close the gap [lb, ub) with the certified solver, pinning the clique to phases 0..lb-1 to break colour-permutation symmetry; the first feasible k is χ, its witness is a SAT model, and minimality is certified either by the clique (k == lb) or by the RUP- Refuted solve at k-1. Either route is certified end-to-end.