The Krawczyk homotopy method of Duff and Lee (ISSAC 2024) certifies predictor-corrector tracking of solution paths of parameter homotopies by a parametric Krawczyk interval test, but its correctness and termination theory is proved only under two idealizations: the system must be affine-linear in the parameters, and interval arithmetic is assumed exact (a real RAM model, i.e., an idealization of computation with exact real numbers). The problem is to extend these guarantees to homotopies with genuinely nonlinear parameter dependence and to floating-point interval arithmetic with outward rounding of endpoints. The direct follow-up literature (Lee 2025) retains both restrictions; a concurrent algorithm of Guillemot and Lairez attains certified tracking with proven termination for nonlinear parameter dependence in an adaptive-precision floating-point model, but by a different method that does not extend the explicit termination theory of the Krawczyk homotopy itself. The extension therefore remains open.

Background

Numerical homotopy continuation is the workhorse of numerical algebraic geometry. To solve a system F(x)=0F(x)=0, one deforms a start system G(x)=0G(x)=0 with known solutions into it through a homotopy H(x,t)H(x,t), t∈[0,1]t\in[0,1], and follows each solution path x(t)x(t) from t=0t=0 to t=1t=1 with a predictor–corrector iteration. In the parameter homotopy variant, the system is a parametrized family F(x;p)F(x;p) and one tracks along a parameter path p(t)p(t) from start parameters p0p_0, where solutions are known, to target parameters p1p_1. Because an approximate path can silently jump to a different solution branch, certified path tracking augments the iteration with a per-step mathematical certificate that a unique solution path stays inside a computed region. Two certificate families exist: alpha-theoretic methods, based on Smale's α\alpha-theory, which certifies a nearby true zero of an analytic map from three computable quantities (α\alpha, β\beta, γ\gamma) evaluated at an approximate zero (Beltrán–Leykin 2012, 2013; Hauenstein–Haywood–Liddell 2014 for Newton homotopies), and interval-arithmetic methods, which enclose the path in interval boxes (Kearfott–Xing 1994 for step control in continuation). Interval arithmetic computes with intervals guaranteed to contain exact values; in floating point, interval endpoints must be rounded outward (lower endpoints down, upper endpoints up) to preserve this guarantee. The Krawczyk operator Kx,Y(E)=−Y F(x)+(Id−Y ∂F(x+E)) EK_{x,Y}(E)=-Y\,F(x)+(\mathrm{Id}-Y\,\partial F(x+E))\,E, for an approximate solution xx and an approximate inverse Jacobian YY, carries the Moore–Krawczyk property: the inclusion K(E)⊆EK(E)\subseteq E implies that FF has a zero in x+Ex+E, and that zero is unique if additionally the contraction condition 2 ∥Id−Y ∂F(x+E)∥<1\sqrt{2}\,\|\mathrm{Id}-Y\,\partial F(x+E)\|<1 holds (the factor 2\sqrt{2} reflects the complex setting; over the reals, ∥Id−Y ∂F(x+E)∥<1\|\mathrm{Id}-Y\,\partial F(x+E)\|<1 suffices). Duff and Lee (ISSAC 2024) introduced the Krawczyk homotopy: a parametric Krawczyk test that certifies the solution path over a whole time subinterval [t0,t0+dt][t_0,t_0+dt], applicable to general parameter homotopies, unlike alpha-theoretic trackers tied to specific homotopy forms. A tilted variant encloses the path in sheared boxes (parallelepipeds s(t)+Irs(t)+I_r following the predictor segment s(t)s(t)) to reduce conservatism. They prove per-step correctness and finite termination: Theorem 4.1 gives explicit inequalities on the step size dtdt and box radius rr (involving ∥Y∥\|Y\|, a bound LL on the interval enclosure of ∂x2H\partial_x^2 H, and ∥F(1)(x⋆;p1−p0)∥\|F^{(1)}(x^\star;p_1-p_0)\| for the parameter-dependent part F(1)F^{(1)} of FF), and Corollary 4.3 derives uniform lower bounds on dtdt and rr, hence termination in finitely many steps. However, the proof uses two idealizations: (i) FF is affine-linear in pp with p(t)=(1−t)p0+tp1p(t)=(1-t)p_0+tp_1, so Ft+dtF_{t+dt} differs from FtF_t by the exactly controlled term dt⋅F(1)(x;p1−p0)dt\cdot F^{(1)}(x;p_1-p_0); and (ii) interval arithmetic is exact — the analysis, in the authors' words, "assumes exact real number computation", while any real implementation rounds interval endpoints outward. Lee (2025) then gave the first complexity analysis for Krawczyk-based certified tracking — explicit a priori stepsize bounds and an iteration-count bound proportional to the weighted path length (the integral of a condition-dependent weight along the path) — but only for affine-linear parameter homotopies and again in the exact-arithmetic idealization. Independently and concurrently, Guillemot and Lairez (ISSAC 2024) proved correctness and termination for a different Moore-box tracker with Taylor-model predictors, for arbitrary nonlinear parameter dependence given by arithmetic circuits, in an adaptive-precision floating-point interval model; this shows the goal is attainable in principle but leaves the explicit termination theory of the Krawczyk homotopy itself untouched. The unresolved target is that theory, beyond both idealizations.

Problem Statement

Remove the two idealizations under which the correctness and termination theory of the Krawczyk homotopy tracking algorithm (Duff–Lee 2024, baseline Algorithm 1 and tilted Algorithm 3, Theorem 4.1 and Corollary 4.3) is currently proved, by establishing the same guarantees for that algorithm in the following relaxed settings. (a) Nonlinear parameter dependence: for parameter homotopies H(x,t)=F(x;p(t))H(x,t)=F(x;p(t)) in which FF depends genuinely nonlinearly on the parameters pp and/or p(t)p(t) is not a straight-line segment, prove that each successful parametric Krawczyk test still certifies existence and uniqueness of the tracked solution path on its step interval, and that the algorithm terminates in finitely many steps. (b) Floating-point interval arithmetic: establish the same guarantees when every interval operation is performed in finite precision with outward rounding of endpoints, under an explicitly stated computational model (fixed or adaptive precision); in particular, quantify when rounding errors accumulated across the Krawczyk iterations cannot break the inclusion test and cannot drive the step size dtdt below the unit roundoff before t=1t=1. The two relaxations may be treated separately, and may be addressed jointly for the tilted variant; the target is to establish both guarantees simultaneously there, or to identify precisely the additional hypotheses under which each guarantee survives.

References

  1. Timothy Duff and Kisun Lee, "Certified homotopy tracking using the Krawczyk method", Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation (ISSAC 2024), ACM, pp. 274–282, 2024. DOI: 10.1145/3666000.3669699; arXiv:2402.07053; https://doi.org/10.1145/3666000.3669699
  2. Kisun Lee, "A priori bounds for certified Krawczyk homotopy tracking", arXiv preprint arXiv:2512.01355, 2025. DOI: 10.48550/arXiv.2512.01355; https://arxiv.org/abs/2512.01355
  3. Alexandre Guillemot and Pierre Lairez, "Validated numerics for algebraic path tracking", Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation (ISSAC 2024), ACM, pp. 36–45, 2024. DOI: 10.1145/3666000.3669673; arXiv:2401.17973; https://doi.org/10.1145/3666000.3669673
  4. Michael Burr, Jonathan D. Hauenstein, and Kisun Lee, "Certified surface approximations using the interval Krawczyk test", Proceedings of the 2026 International Symposium on Symbolic and Algebraic Computation (ISSAC 2026), ACM, pp. 77–86, 2026. DOI: 10.1145/3815436.3815444; arXiv:2602.07718; https://doi.org/10.1145/3815436.3815444
  5. Timothy Duff and Kisun Lee, "Certifying Galois/monodromy actions via homotopy graphs", arXiv preprint arXiv:2603.17288, 2026. DOI: 10.48550/arXiv.2603.17288; https://arxiv.org/abs/2603.17288
  6. Alexandre Guillemot and John Voight, "Belyi map verification using certified path tracking", arXiv preprint arXiv:2604.15562, 2026. DOI: 10.48550/arXiv.2604.15562; https://arxiv.org/abs/2604.15562
  7. Alexandre Guillemot, "Certified algebraic path tracking with Algpath", ACM Communications in Computer Algebra 59(3):53–56, 2025. DOI: 10.1145/3787957.3787960; https://doi.org/10.1145/3787957.3787960
  8. Carlos Beltrán and Anton Leykin, "Certified numerical homotopy tracking", Experimental Mathematics 21(1):69–83, 2012. DOI: 10.1080/10586458.2011.606184; https://doi.org/10.1080/10586458.2011.606184
  9. Carlos Beltrán and Anton Leykin, "Robust certified numerical homotopy tracking", Foundations of Computational Mathematics 13(2):253–295, 2013. DOI: 10.1007/s10208-013-9143-2; https://doi.org/10.1007/s10208-013-9143-2
  10. Jonathan D. Hauenstein, Ian Haywood, and Alan C. Liddell Jr., "An a posteriori certification algorithm for Newton homotopies", Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation (ISSAC 2014), ACM, pp. 248–255, 2014. DOI: 10.1145/2608628.2608651; https://doi.org/10.1145/2608628.2608651
  11. R. Baker Kearfott and Zhaoyun Xing, "An interval step control for continuation methods", SIAM Journal on Numerical Analysis 31(3):892–914, 1994. DOI: 10.1137/0731048; https://doi.org/10.1137/0731048