Exact Formulation and Algebraic Certification Framework for Mixed-Integer AC Optimal Power Flow

This Preprint formulates an exact algebraic certification framework for a finite-horizon mixed-integer alternating-current optimal power flow (AC OPF) problem. The feasible set is constructed as a finite union of disconnected non-convex semialgebraic strata. Discrete components are encoded exactly by polynomial equalities, specifically u^2 - u = 0 for binary variables and pc * pd = 0 for storage complementarity. The framework operates directly on the non-convex geometry by explicitly rejecting convex relaxations, piecewise linearization, integer smoothing, and time decomposition methods. The methodology establishes a Fritz John stationarity system rather than a Karush-Kuhn-Tucker (KKT) system to account for potential failures of the linear independence constraint qualification (LICQ) on alternating-current power-flow boundaries. The framework maps an initial global square system of 49 variables and 49 equations down to two smaller leaf systems for computer algebra processing. No polynomial-time complexity is claimed; the approach isolates exact polynomial systems for hardware certification. Network Topology and Rectangular Equations The framework evaluates a 5-bus benchmark network evaluated over a discrete-time horizon of t = 0, 1. The network components include: Bus 1 acts as the slack bus with fixed voltage V_1 = 1 + j0. Bus 2 functions as a continuous PQ/PV generation node with active power bounds of [0, 1]. Buses 3 and 5 are PV nodes equipped with binary generators. Bus 4 integrates a temporal storage system with charging and discharging bounds. The lines possess series impedance z = 0.1 + j0.5, translating to a line admittance y_line = 5/13 - j25/13. All variables are represented in rectangular coordinates (V_i,t = x_i,t + j y_i,t), ensuring every AC power-flow constraint remains a polynomial equation with rational coefficients. Exact Semialgebraic Feasible Set and Prohibited Methodologies The exact formulation enforces binary assignments (u_3,t, u_5,t) and storage power boundaries without logical inequalities. The storage system yields three disjoint semialgebraic operating strata: charging (pc > 0, pd = 0), discharging (pc = 0, pd > 0), and idle (pc = 0, pd = 0). Continuous inequality constraints consist of bus voltage magnitude bounds (e.g., x_3,t^2 + y_3,t^2 = 441/400 and x_5,t^2 + y_5,t^2 = 1), generator reactive bounds, storage energy bounds, inter-temporal ramping constraints, and line-current bounds. To preserve the exact mathematical topology, the framework defines explicit methodological boundaries. The following techniques are excluded from the main algorithmic path: Convex relaxations (e.g., McCormick envelopes, Semidefinite/Second-Order Cone programming), as they alter the disconnected nature of the binary strata. Piecewise linearization, which introduces artificial local minima. Continuous-integer smoothing, which connects isolated binary points via a penalty function. Time decomposition, which breaks exact storage coupling between temporal periods. Moment-SOS/Lasserre hierarchy as a primary search mechanism. Raw polyhedral homotopy and raw elimination without Rational Univariate Representation (RUR). Sparse toric resultants, comprehensive Grobner systems, and perfect elimination ordering used as general complexity bounds. Fritz John Ideal Construction and Polynomial Reductions Because the rectangular power-flow Jacobian can become singular at saddle-node bifurcation points, the framework applies a cone-preserving Fritz John stratification. This avoids discarding critical stationary points when LICQ fails. The unreduced global system incorporates 22 physical equalities, active inequalities, 26 Fritz John stationarity equations, and 1 multiplier normalization equation. Through branch-free linear combinations, variables including the Bus-2 active generation, Bus-3 and Bus-5 reactive generation, and storage energies are eliminated via exact topological projection. This decreases the system size from 49 to 31 variables. The spherical multiplier normalization constraint is replaced by affine projective patches to eliminate a dense 23-variable multiplier clique. Following a storage affine substitution, a temporal decoupling lemma proves that the equality generators for t = 0 and t = 1 become algebraically isomorphic under a fixed binary and storage stratum, shifting temporal coupling entirely into inequality filters and objective aggregation. Surviving Leaf Systems and Interval Branch-and-Bound The algebraic reductions produce two terminal systems for leaf certification: Regular KKT Patch: A structurally square ideal operating in a polynomial ring with 28 + |A| variables. Singular Primal Locus: A multiplier-free determinantal ideal processed purely in the 16-variable primal space via the active constraint Jacobian. Exhaustive stratification requires parsing 144 independent binary and storage strata combinations. The branch-and-bound logic isolates boxes using outward-rounded rational interval arithmetic and exact geometric contractors, including a Bus-2 active generation contractor, line-circle contractors for buses 3 and 5, a generalized Krawczyk operator, and an inter-temporal ramping contractor mapping to a branch-free algebraic discriminant. Leaf Certification Pipeline Once a topological leaf is verified, it enters a dual-track master-worker algebraic pipeline. The framework executes the following sequential algorithms: Modular Grobner Basis: Prevents coefficient swell via finite prime field computations and rational reconstruction using the Chinese Remainder Theorem. Primal Polar Limit: Resolves positive-dimensional components within the Singular Primal Locus without generic rank assumptions by extracting the exact algebraic limit of a symbolic moment curve. Rational Univariate Representation (RUR) via Quotient Ring Trace Operators: Bypasses FGLM conversion complexity by extracting coordinate mappings via trace forms of multiplication operators constructed from standard monomial bases. Primitive Element Field Resolution: Reconstructs dependent physical network states (e.g., active generation setpoints) as univariate polynomials to prevent numerical drift. Real Root Isolation: Computes exact rational intervals for real roots using Sturm-Habicht sequences. Inactive Inequality Filtering: Certifies continuous physical bounds via exact rational Bernstein projection and de Casteljau subdivision over isolating intervals. Rational Positivstellensatz Global Certificate: Evaluates an exact rational sum-of-squares representation to provide a mathematical proof of the objective lower bound, mapping constraint degrees to the D'Acunto-Kurdyka Lojasiewicz exponent. Complexity and Computational Scope The worst-case complexity of the branch-and-bound tree is combinatorial and exponential. For the algebraic certification, the 14-variable regular patch is analyzed utilizing sparse chordal elimination. The perfect elimination ordering demonstrates a treewidth of 6, and the exact chordal Bernshtein-Kushnirenko-Khovanskii (BKK) bound limits the complex root count strictly to 8192 roots. Thus, the computational complexity of the trace-based RUR scales to O(8192^3) rational operations. The intended hardware specification requires a 64-core x86-64 Linux environment with 512 GB of RAM minimum and 500 GB of scratch storage, processing exact symbolic routines via Singular and Maple. Keywords: Mixed-Integer AC Optimal Power Flow, Exact Algebraic Certification Framework, Fritz John Stationarity System, Non-Convex Semialgebraic Strata, Modular Gröbner Basis Computation, Rational Univariate Representation, Primal Polar Limit, Positivstellensatz Certificate, Interval Branch-and-Bound, Schreyer Syzygy Matrix, Semialgebraic Geometry, Exact Interval Arithmetic, Polynomial Ideal Theory, Algebraic Certification.