Exactly Verified Optimality Intervals for the Small PGLib-OPF Cases

Replayable Branch-and-Bound Records with Rational Certificates For the 9 PGLib-OPF v23.07 cases with at most 14 buses (case3_lmbd, case5_pjm and case14_ieee in the typical, congested and small-angle-difference sets) we report rational intervals [L, U] that contain the optimal value of the declared AC optimal power flow model. Rounded upward, the smallest and largest relative widths are 8.0×10^-11 and 3.8×10^-8; for the same cases in our earlier catalogue (doi:10.5281/zenodo.23592205) the corresponding upward-rounded extrema are 7.5×10^-7 and 7.4×10^-2. Every interval reported here has strictly smaller relative width than its counterpart there, and every one lies inside the rounding interval of PGLib's published five-significant-digit AC objective, so the global optimum rounds to the published value in every case. Lower bounds, cutoff-dependent bound tightenings and exclusions are exact rational certificates in a recorded spatial branch-and-bound tree over voltage boxes. Upper bounds are supported by interval-existence certificates for the unbranched equality system, verified limit and cost enclosures, and a separate exact-interval angle lift establishing compatibility with the unwrapped branch limits. A checker that calls no optimisation solver replays every record from its files (6299 certificates over 2769 nodes, 53 s in total), verifies tree coverage and certificate arithmetic, and recomputes each interval, including for records with open terminal nodes. It rejects every record of a released suite of tampered records in 14 categories. The results certify objective-value intervals; they do not assert exact optimal values, nor that the intervals are the narrowest obtainable. Files small_cases_certified.pdf: the paper. zenodo_pglibsmall_v1.0.0_2026-10-24.zip: the verification bundle: the checker program ac-verify (source, no producer code), for each of the nine cases the branch-and-bound record (event file, boxes, certificates, incumbent boxes), exact rational endpoints, the four figures, the rejection suite, the rigorous angle-lift script, the number and figure generators, the PGLib-OPF v23.07 case files and baseline file with attribution, and the earlier catalogue's endpoints and PowerModels re-solve output used for comparison. 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 (a few minutes) rebuilds ac-verify from source, replays every record from its files alone, runs the angle lift and the rejection suite, and regenerates the endpoints and every number of the paper; it exits non-zero on any failure. Needs a Rust toolchain, Python 3 and zsh. 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 data retain CC BY 4.0 with attribution in data/ATTRIBUTION.md. The software that produced the records is proprietary and not distributed. Commercial-use enquiries: labs@smartledger.solutions. No patent licence is granted by this release. Applied work: certified assurance for power-system optimisation — energy.smartledger.technology