Smale's alpha theory certifies that a numerical point is an approximate solution of a square analytic system by checking α(F,x) = β(F,x)γ(F,x) < (13−3√17)/4, but its classical implementations need costly exact arithmetic. Lee's ICMS 2024 framework 'alpha theory over regions' replaces the point x by an interval box I and computes α(F,I), β(F,I), γ(F,I) with interval arithmetic, achieving large empirical speedups over exact-arithmetic certification for polynomial systems. The framework, however, rests on unproven practical heuristics: the interval enclosure of the inverse Jacobian has no tightness or near-singularity guarantee, the region-wise upper bound for γ(F,I) is available only for polynomial systems, no formal complexity comparison with exact-arithmetic alpha certification exists, and the box radius and working precision must be chosen by hand. This problem asks to close these gaps jointly: derive region-wise gamma bounds for structured nonpolynomial analytic classes (at least polynomial–exponential and D-finite systems), characterize achievable enclosure quality for interval Jacobian inverses, provide a formal complexity analysis comparing interval-based and exact-arithmetic alpha certification, and design an adaptive radius/precision selection algorithm with proved termination and success guarantees — yielding a complete, self-driving, complexity-understood region-wise alpha certification procedure.
Background
A basic task in numerical algebraic geometry is to certify that a candidate numerical solution of a square system (each analytic on an open set ) really corresponds to an exact solution. The Newton operator is , where is the Jacobian matrix; a point is called an approximate solution of if repeated Newton iteration converges quadratically (the distance to the associated exact solution at least squares each step) to . Smale's alpha theory gives a computable sufficient criterion: with the Newton-step norm and measuring the size of all higher derivatives relative to the Jacobian (here is the tensor of -th order partial derivatives), the test certifies that is an approximate solution, while additionally certifies that two nearby points converge to the same solution. The software alphaCertified (Hauenstein–Sottile) implements this test, but rigorous use requires exact rational arithmetic, which becomes expensive for large or ill-conditioned systems. The Krawczyk method, the main alternative, uses interval arithmetic — arithmetic on intervals , which computes conservative enclosures — to prove that the Newton operator contracts a box onto itself; it certifies existence and uniqueness of a solution in a box but gives no quadratic-convergence statement, which alpha theory does.
Lee (ICMS 2024) combined the two ideas into 'alpha theory over regions': for an interval vector (box) , define with and . The same numerical thresholds then certify that every point of is an approximate solution converging to one common associated solution, and boxes can be certified as containing equal or distinct solutions. For polynomial systems, the hard quantity is bounded using the classical Shub–Smale approach: with the Bombieri–Weyl norm (a degree-weighted coefficient norm of the polynomial system), the maximum degree , the diagonal scaling matrix with entries , and the condition-type quantity , one obtains the region-wise bound , reducing the supremum over the box to interval evaluations. The implementation evaluates and with the arbitrary-precision interval library MPFI, and encloses the inverse Jacobian over the box — an inverse interval matrix, i.e. an interval matrix containing — by interval LU decomposition with partial pivoting performed in Kaucher arithmetic, a generalized interval arithmetic whose 'dual' intervals form groups under addition and multiplication and which can return tighter inverse enclosures than classical interval arithmetic, followed by iterative refinement of interval linear systems. Experiments (cyclic-6 roots, Fano problems with up to 47104 solutions) show order-of-magnitude wall-clock speedups over alphaCertified with exact arithmetic.
The framework stops at the proof of concept. Four theoretical gaps are evident from the paper. (1) The Kaucher-LU-plus-refinement procedure 'may return a tighter' inverse enclosure but comes with no guarantee of near-optimal tightness, and the behavior when interval Jacobian entries approach singularity is unanalyzed; this matters because enclosing quality directly inflates and and can silently destroy a certificate. (2) The region-wise bound exists only for polynomial systems, while point-wise bounds are known for polynomial–exponential systems (systems whose equations mix polynomials and exponentials of polynomial expressions; Hauenstein–Levandovskyy) and for systems involving univariate D-finite functions (functions satisfying linear ODEs with polynomial coefficients, also called holonomic; Burr–Lee–Leykin) — the region-wise versions do not exist. (3) The comparison with exact-arithmetic certification is purely empirical. (4) The box radius and working precision are chosen by hand, and no adaptive procedure with termination guarantees is given, although the point-based software alphaCertified already raises its internal working precision automatically to control floating-point error, and adaptive multiprecision strategies are standard in certified path tracking. Notably, an exact (optimally tight) inverse interval enclosure is out of reach in general: Poljak and Rohn proved that deciding robust nonsingularity of an interval matrix (whether every real matrix in it is nonsingular) is NP-hard, and a singular member makes unbounded, so exact tightness would decide an NP-hard problem — the realistic target is a quantified sufficient-tightness guarantee.
Problem Statement
Place region-wise interval-arithmetic alpha-theoretic certification on the same rigorous footing as classical point-based alpha theory, by resolving the following four interdependent gaps in Lee's 'alpha theory over regions' framework. The components are linked facets of one objective — a complete, adaptive, complexity-understood region-wise alpha certification algorithm for broad classes of analytic systems. The four gaps are interdependent components of this single objective, to be resolved jointly.
(1) Enclosure quality for the interval Jacobian inverse. For the computation of , establish a rigorous guarantee: either a provable approximation-quality bound on the returned enclosure relative to the tightest possible one, or a characterization of what can and cannot be guaranteed in polynomial time — given that exact tightness would decide the NP-hard problem of robust nonsingularity — together with an analysis of the failure modes and stability when contains nearly singular matrices.
(2) Region-wise gamma bounds beyond polynomial systems. Extend the region-wise upper bound to structured analytic classes for which only point-wise bounds are known: derive region-wise upper bounds with an explicitly quantified tightness guarantee (tightness measured against the true region-wise value ) for at least polynomial–exponential systems and systems involving univariate D-finite functions, with certified interval evaluation of the required derivative data over boxes.
(3) Formal complexity comparison. Provide a rigorous cost model and analysis comparing region-wise interval-alpha certification (arbitrary-precision interval arithmetic with LU-based inversion) against exact-arithmetic alpha certification: operation counts or bit-complexity in terms of system size, degree/ODE order, conditioning, box radius, and precision, and a characterization of the regimes in which each approach wins or the interval-based one underperforms.
(4) Adaptive certification algorithm. Design and prove correct an adaptive procedure that, given a candidate approximate solution (and a system in the classes of (2)), automatically selects the interval radius and the working precision by a stated criterion, with a termination guarantee: whenever the underlying point-wise alpha test succeeds at the candidate point, i.e. , the procedure terminates and returns a valid region-wise certificate on a non-degenerate box of positive radius (the zero-radius point box does not satisfy the guarantee) at a box radius and working precision it selects, together with an explicit positive lower bound on that radius and a complexity bound on its cost.
References
- Kisun Lee, Effective alpha theory certification using interval arithmetic: alpha theory over regions, Mathematical Software – ICMS 2024, Lecture Notes in Computer Science 14749, pp. 275–284, Springer, 2024. DOI: 10.1007/978-3-031-64529-7_29; arXiv:2405.04842, https://arxiv.org/abs/2405.04842
- Michael Burr, Kisun Lee, Anton Leykin, Effective Certification of Approximate Solutions to Systems of Equations Involving Analytic Functions, Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation (ISSAC 2019), pp. 267–274, 2019. DOI: 10.1145/3326229.3326235; arXiv:1901.10384, https://arxiv.org/abs/1901.10384
- Jonathan D. Hauenstein, Viktor Levandovskyy, Certifying solutions to square systems of polynomial-exponential equations, Journal of Symbolic Computation 79, pp. 575–593, 2017. DOI: 10.1016/j.jsc.2016.07.020; arXiv:1109.4547, https://arxiv.org/abs/1109.4547
- Jonathan D. Hauenstein, Frank Sottile, Algorithm 921: alphaCertified: certifying solutions to polynomial systems, ACM Transactions on Mathematical Software 38(4), pp. 1–20, 2012. DOI: 10.1145/2331130.2331136; arXiv:1011.1091, https://arxiv.org/abs/1011.1091
- Michael Shub, Steve Smale, Complexity of Bézout's theorem. I. Geometric aspects, Journal of the American Mathematical Society 6(2), pp. 459–501, 1993. DOI: 10.1090/s0894-0347-1993-1175980-4, https://www.ams.org/journals/jams/1993-06-02/S0894-0347-1993-1175980-4/
- Svatopluk Poljak, Jiří Rohn, Checking robust nonsingularity is NP-hard, Mathematics of Control, Signals and Systems 6(1), pp. 1–9, 1993. DOI: 10.1007/BF01213466, https://link.springer.com/article/10.1007/BF01213466
- Paul Breiding, Kemal Rose, Sascha Timme, Certifying Zeros of Polynomial Systems Using Interval Arithmetic, ACM Transactions on Mathematical Software 49(1), pp. 1–14, 2023. DOI: 10.1145/3580277; arXiv:2011.05000, https://arxiv.org/abs/2011.05000
- Timothy Duff, Kisun Lee, Certified homotopy tracking using the Krawczyk method, Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation (ISSAC 2024), pp. 274–282, 2024. DOI: 10.1145/3666000.3669699; arXiv:2402.07053, https://arxiv.org/abs/2402.07053
- Kisun Lee, A priori bounds for certified Krawczyk homotopy tracking, preprint, 2025. arXiv:2512.01355, https://arxiv.org/abs/2512.01355
- Michael Burr, Jonathan D. Hauenstein, Kisun Lee, Certified surface approximations using the interval Krawczyk test, Proceedings of the 2026 International Symposium on Symbolic and Algebraic Computation (ISSAC 2026), pp. 77–86, 2026. DOI: 10.1145/3815436.3815444; arXiv:2602.07718, https://arxiv.org/abs/2602.07718
- Timothy Duff, Kisun Lee, Certifying Galois/monodromy Actions via Homotopy Graphs, preprint, 2026. arXiv:2603.17288, https://arxiv.org/abs/2603.17288
- Paul Breiding, Taylor Brysiewicz, David K. Johnson, Low-Memory Numerical Certification, preprint, 2026. arXiv:2604.16623, https://arxiv.org/abs/2604.16623
- Xiaojie Dou, Jin-San Cheng, Junyi Wen, A Maple Implementation for Deterministically Certifying Isolated Simple Zeros of Over-Determined Polynomial Systems with Interval Arithmetic and Its Applications, AppliedMath 6(1), article 15, 2026. DOI: 10.3390/appliedmath6010015, https://doi.org/10.3390/appliedmath6010015