Certified Fractional Chromatic Bounds from Implicit Column Generation

Author's submitted manuscript (version of 17 August 2026). Submitted for publication; not peer reviewed. Dold et al. (CP 2026) equip ZykovColor with VeriPB proof logging and the CakePB checker, leaving one lower-bounding technique uncertified: the fractional chromatic number bound obtained from LP duality and column generation, because VeriPB cannot reason about rational values. This paper supplies a certificate interface for that bound. Writing a rational dual candidate as y_v = p_v/D with integer p_v ≥ 0 and D > 0, full dual feasibility is equivalent to the integer condition max_S Σv∈S p_v ≤ D over stable sets S. A machine-verifiable proof of that single inequality certifies the fractional lower bound and its integer ceiling without logging restricted masters, generated columns, or numerical dual iterates. On 116 DIMACS instances and 1,000 Erdős–Rényi graphs, 1,041 endpoints pass the complete formal chain. Supporting code, per-instance results, manifests, and full-evidence proof archives are archived separately at DOI 10.5281/zenodo.21981971.