Recursive three-parameter upper-bound construction

This module re-exports the vendored formalization imported from 2-coloring-1-round.