Certified Continuation Power Flow: Computer-Assisted Proofs of Loading Margins under Generator Limits

A continuation power flow decides from floating-point data when generators switch between voltage control and reactive-power limits, and one wrong decision can change the loading margin far beyond any tolerance. We present a certified continuation power flow. For a given base point, load direction and generator participation, it establishes by a computer-assisted proof the discrete structure of the quasi-static trajectory: which generators reach their limits and in which order, including returns to voltage control, and how it ends: at a saddle-node or limit-induced bifurcation, at reserve exhaustion, or at a voltage limit. The terminal loading is enclosed to the resolution of double-precision (binary64) numbers. Kantorovich tubes cover the continuous part, in an admittance-weighted energy norm in which the curvature of the power-flow map is bounded by a constant set by the norm; switching points are certified as regular zeros of square augmented systems, the first turning point by strict concavity of the loading. The proofs assume a correct program and floating-point library and, on the three largest of eight test systems (up to 3012 buses), an a priori error bound of a banded factorization. The paths of a floating-point continuation power flow with a consistency test were certified in 352 of 362 runs; the others, next to a degenerate load direction, were declined. Two constructed switching rules without the test miss the certified end in more than half of their runs, and MATPOWER's margins differ through its modelling rules. The certified trajectories are reference solutions for such programs. Preprint, not peer reviewed. Code and results: https://doi.org/10.5281/zenodo.24126076