Exact Certificates for AC Optimal Transmission Switching

Kernel-Checked Small-Instance Enumeration and Rationally Checked All-Topology Bounds up to 500 Buses We present an exact-rational certification pipeline for a declared current-limited AC optimal transmission-switching model in rectangular voltage coordinates, with current limits at both line ends (including charging current) and principal angle-difference limits of ±30° on in-service lines. Numerical solvers supply untrusted certificate candidates; exact checking establishes topology-wise lower bounds, infeasibility and feasible-point upper bounds, with no tolerance. Lower bounds are Lagrangian certificates whose diagonal shift is paid for by coordinate caps derived from the model rows. On the six-line PGLib case5 data, complete enumeration of the 64 topologies (42 eliminated, 22 bounded) yields the certified objective interval [15015.074617, 15015.074821], and strictly separates one topology from all alternatives, establishing it as the unique globally optimal topology for this model; the optimal value of switching lies in [1145.375358, 1149.968972]. Exact Rust replay and independent physical checking of feasible witnesses certify a unique optimal topology at each of five sampled current-limit scales; it opens line 3–4 at scales 0.8, 0.9 and 1.0 and keeps all lines in service at 1.1 and 1.2. Across case3 and case5, Lean kernel replay verifies all 72 emitted leaf certificates, topology-indexed lower-bound aggregation and separation, derivation of coordinate caps from rows, and exact rational feasible witnesses with encoded true-angle checks and costs; the audited declarations use only propext, Classical.choice and Quot.sound. Correspondence between the emitted data and the physical instances remains outside Lean and is supported by the paper proof and independent exact checks. Beyond enumeration, interval-existence certificates for feasible points, a disaggregated switched-line relaxation and a PSD certificate checked by sparse multiplication give exactly checked (not yet Lean-replayed) all-topology intervals under the PGLib apparent-power model on case57, case118 and case500_goc, of relative width at most 0.43%, 0.51% and 0.94%, from root bounds alone, a certified positive switching benefit on case57 and case118, and a comparison with the global solver SCIP under the same symbolic formulation. Files ac_ots_certificates.pdf: the paper. zenodo_acots_v1.0.0_2026-10-23.zip: the certificate bundle (repository layout): the checker program ac-verify (source, no producer code), exported rational certificates, feasible points and interval-existence boxes, independent physical evaluator and row cross-check, rejection suite, number and table generators, PGLib case data with attribution, and the Lean 4 project with axiom-audit logs. 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 rebuilds ac-verify from source, replays every certificate, point and box from the files alone, runs the physical checks, row cross-check and rejection suite, and regenerates every number and table of the paper; LEAN=1 ./replay.sh adds the Lean kernel build and axiom audit (about an hour). Needs a Rust toolchain and Python 3; the Lean step needs elan. 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 certificate producers are proprietary and not distributed. Commercial-use enquiries: labs@smartledger.solutions. No patent licence is granted by this release.