Certified Optimality Intervals for the PGLib-OPF Benchmark Library

Exact Optimal-Value Enclosures for 60 PGLib-OPF Cases and Consistency Checks Against 180 Baseline Reports The PGLib-OPF library is the standard benchmark for AC optimal power flow, and its published baseline reports, for each case, the objective value of a local AC solution and the optimality gaps of the QC and SOC relaxations. These are floating-point outputs without certificates. For every typical (TYP), congested (API) and small-angle-difference (SAD) case of PGLib-OPF v23.07 with at most 600 buses — 60 cases — we give an interval $[L, U]$ that provably contains the optimal value of the declared AC model: L from a Lagrangian certificate of a semidefinite relaxation verified by exact rational multiplication, and U from a rational box in which a Krawczyk-type test proves that a solution of the true (irrational) AC equations exists and satisfies every limit. Per-branch angle limits and phase shifters enter through rigorous rational enclosures of the trigonometric coefficients. Every certificate replays from its file with a small checker that contains no optimisation code. None of the 180 rounded baseline reports is ruled out by interval separation against these enclosures. The enclosures determine the optimal value to the five printed digits for 12 cases, each agreeing with the published value, and have relative width at most 1% for 35 cases and at most 11.63% overall. The exact lower bound lies strictly above the published QC estimate on 49 cases and above the published SOC estimate on 55. For every certified point we also prove, in exact interval arithmetic over the whole certified box, that real bus angles exist satisfying every unwrapped branch angle limit. A separate floating-point evaluation of our certificate box centres using PowerModels v0.19.9, the baseline's software, gives small constraint residuals. Re-solving with that software reproduces all 60 published five-digit AC values; on 8 cases, the returned numerical objective is below our certified lower bound, and the returned point has a numerically detected limit violation. Files pglib_catalogue_certificates.pdf: the paper. zenodo_pglibcat_v1.0.0_2026-10-23.zip: the certificate bundle: the checker program ac-verify (source, no producer code), for each of the 60 cases the exported lower-bound certificate, box certificate and replay output, exact rational endpoints, the rigorous angle-lift script and output, the rejection suite, the independent row cross-check, the PowerModels v0.19.9 evaluation (scripts, pinned Julia manifest, outputs, solver points and Ipopt logs), number and table generators, and the PGLib-OPF v23.07 case files and baseline file with attribution. Its SHA-256 is in the adjacent .sha256 file; SHA256SUMS inside covers every file. README.md, LICENSE.md: copies of the bundle's front matter. Verification ./replay.sh (about 15 minutes) rebuilds ac-verify from source, replays every certificate and box from the files alone, runs the rejection suite and the row cross-check, re-runs the rigorous angle lift, and regenerates the table, endpoints and every number of the paper; it exits non-zero on any failure. PM=1 ./replay.sh also re-runs the PowerModels evaluation (Julia 1.10). Needs a Rust toolchain and Python 3. Hardware of the recorded runs: Apple M3 Pro, 18 GiB. Licences: new author-owned material is licensed by SmartLedger Solutions under CC BY-NC 4.0 (LICENSE.md). PGLib-OPF case files and baseline file retain CC BY 4.0 with attribution in data/ATTRIBUTION.md. The certificate producers are proprietary and not distributed. Commercial-use enquiries: labs@smartledger.solutions. No patent licence is granted by this release.