Independently Checkable Certificates for Connected DC Optimal Transmission Switching

We present independently checkable objective-bound certificates for connected DC optimal transmission switching with rational data and linear generation costs. Certificates establish feasible upper bounds and globally valid lower bounds without trusting the producer. Lean 4 proves interval soundness and tolerance closure for a reflected checker; <!--n:n_artifacts-->11<!--/n--> certificate artifacts have kernel-checked acceptance and source-parsing statements. For the IEEE 118-bus instance with uniform 120 MW limits, a certificate containing <!--n:closed_records-->97<!--/n--> tree records reduces the <!--n:prev_rel_pct-->0.39<!--/n--> % gap left open in earlier work by the authors (<!--n:prev_L-->86119.999998302<!--/n--> ≤ OPT ≤ <!--n:prev_U-->86456.301639772<!--/n-->) to an absolute gap of at most <!--n:closed_gap-->5.33e-10<!--/n-->. At 135 and 150 MW, root certificates prove gaps of at most <!--n:gap_u135-->2.00e-5<!--/n--> and <!--n:gap_u150-->3.07e-5<!--/n-->. A separately kernel-checked residual-witness theorem certifies the existence of exactly feasible DC flows without constructing exact angle coordinates. Its implementation enables exact-rational program replay of objective intervals through <!--n:approx_buses_last-->78478<!--/n--> retained buses of PGLib-OPF-derived models. On the largest instance, root production, angle construction and replay took <!--n:approx_root_s_pglib78484-->322.25<!--/n-->, <!--n:approx_angles_s_pglib78484-->10.19<!--/n--> and <!--n:approx_replay_s_pglib78484-->477.22<!--/n--> seconds, with a maximum recorded stage peak memory of <!--n:approx_peak_mib_pglib78484-->1272<!--/n--> MiB. These large certificates establish verification scale using economic-dispatch lower bounds; their acceptance is replay-checked, not kernel-checked. Replay also certifies one-opening gaps of at most <!--n:gap_e1_300-->4.39e-4<!--/n--> and <!--n:gap_e1_1354-->0.0122<!--/n--> at 300 and 1,354 buses, a two-opening improvement of at least <!--n:sep_e2_e1-->701.854583<!--/n--> at 300 buses, and, at both sizes, that unrestricted switching improves on every single-line opening, by at least <!--n:sep_unr_e1_pglib300-->3353.758201<!--/n--> and <!--n:sep_unr_e1_pglib1354-->4820.479329<!--/n-->. All reported production, replay and kernel checks ran on one Apple M3 Pro laptop with 11 cores and 18 GB of memory. Guarantees concern the declared connected DC models, not AC feasibility or contingency security. Contents of the bundle paper/ — the manuscript (Markdown source and PDF). certs/ — the eleven certificates of Table 2 (JSON lines); data/ots/ — the four MATPOWER-format source files they refer to. certs/scale/ — the certificates of the scaling study (300 to 78,478 buses), each replayed in the paper; data/pglib/ — the PGLib-OPF-derived instances with their conversion records and ATTRIBUTION.md (copyright holders and requested citations of the sources); tools/scale/ — the declared converter (rules R1–R8). verifier/ — the exact-rational replay program (verify_ots.py, its streaming wrapper verify_ots_stream.py) and its mutation tester; verifier v2 (verify_ots_v2.py, exact or residual-bounded witness angles); the independent residual-witness checker (check_residual_witness.py) and the adversarial tests of the residual rule (adversarial_residual.py). lean/ — the Lean 4 project: the model, the soundness proofs, the reflected replay, the 11 certificate artifacts with their source-correspondence modules, and Audit.lean, which prints the axioms of every certificate theorem and of the two residual-rule theorems. tests/golden/ — the expected replay outcomes, the Lean manifest and the outward decimals; tests/evidence/compare_u120_logs/ — the solver logs of Table 3; tests/paper_numbers.py — the generator of the tables; tests/paper_figures.py — the generator of the figures; tests/evidence/scale/ — the scaling-study logs, replay outputs, residual checks and conversion audit; tests/golden/scale_replays.jsonl — the expected scale replays. The certificate producer and the witness-search tools are not part of the release; the release reproduces verification, not production. replay.sh, REPLAY.md, REPLAY_REPORT.md — the automated replay, its commands and the report of its run on the staging copy of this bundle. AUDIT_AXIOMS.txt — the axiom audit; SHA256SUMS — the SHA-256 manifest for the release files it lists. Verification ./replay.sh checks the release manifest when present; replays the eleven Table 2 certificates and the twenty scaling-study certificates against their golden verdicts and exact bounds; runs the mutation tester; checks byte-for-byte regeneration of the shipped Lean artifacts from the released certificates; regenerates and compares the manuscript tables; and, when enabled and lake is available, builds the Lean project one module at a time and checks its axiom audit. It writes REPLAY_REPORT.md. The Lean step needs about 8 GB of memory per 118-bus module group and several hours on the hardware above; LEAN=0 ./replay.sh skips it and SCALE=0 skips the scaling-study certificates. REPLAY.md lists the commands. Inspect REPLAY_REPORT.md for both failures and skipped steps. A run with LEAN=0, or with the Lean step skipped because lake is unavailable, does not rerun the kernel checks. The shipped report records the run on the staging copy of this bundle: certificate replay, Lean builds and axiom audit passed; the checksum step was skipped there because SHA256SUMS is written when the bundle is sealed. The independent residual-checker and adversarial-test results are recorded in the evidence files; replay.sh does not rerun those tests; step 6 of REPLAY.md reruns the residual checker, and verifier/adversarial_residual.py (usage in its header) reruns the adversarial tests. Kernel checking establishes statements about the embedded Lean objects and parsed source bytes; their correspondence to the released certificate files is checked by regeneration, not proved in the kernel. Acceptance of the scaling-study certificates rests on the exact-rational replay programs; the separately formalised residual-witness theorem does not kernel-check those certificates. The mutation tester is implementation testing, not an exhaustive correctness proof. Integrity: shasum -a 256 -c SHA256SUMS inside the bundle; the SHA-256 of the tarball is in the .sha256 file beside it. Environment Python: 3.13.7 (standard library only for the replay; tests/paper_numbers.py also standard library) Lean: leanprover/lean4:v4.33.1 with Mathlib v4.33.1 (lean/lake-manifest.json pins the dependencies) hardware: Apple M3 Pro, 18 GiB (hardware.json) Licences: Except for separately licensed verifier files and third-party material, the new author-owned material is licensed by SmartLedger Solutions under CC BY-NC 4.0. See LICENSE.md and verifier/VERIFIER_LICENSE.md for scope and exceptions. Third-party material retains its applicable licences and attribution, including PGLib-OPF-derived data under CC BY 4.0 (copyright holders and requested citations in data/pglib/ATTRIBUTION.md). Commercial-use permission for material covered by CC BY-NC 4.0 may be requested at labs@smartledger.solutions. The certificate producer is proprietary and not distributed. No patent licence is granted by this release.