Computer-assisted proofs for finding the monodromy of Picard-Fuchs differential equations for a family of K3 toric hypersurfaces

TL;DR

The authors address the monodromy problem for a PF differential equation arising from a two-parameter family of K3 toric hypersurfaces by developing a computer-assisted proof framework that combines interval arithmetic with rigorous ODE continuation. They construct a Pfaffian representation, compute a rigorously enclosed fundamental system at a base point, and perform analytic continuation along six loops encircling singularities to obtain six monodromy matrices, proving the monodromy problem for this PF equation. A key result is that the monodromy matrices lie in GL_4(ℤ) and generate the monodromy group, with unimodularity ensuring integer entries and enabling a unique determination of the monodromy from the rigorous enclosures. The framework relies on validated numerics (including DD precision) and a Taylor-series–based rigorous integrator, illustrating a path toward computer-assisted proofs in complex differential equations arising from algebraic geometry and string theory. The work highlights how combining Pfaffian formulations, interval arithmetic, and validated analytic continuation can rigorously resolve global properties of differential systems tied to geometric moduli.

Abstract

In this paper, we present a numerical method for rigorously finding the monodromy of linear differential equations. Beginning at a base point where certain particular solutions are explicitly given by series expansions, we first compute the value of fundamental system of solutions using interval arithmetic to rigorously control truncation and rounding errors. The solutions are then analytically continued along a prescribed contour encircling the singular points of the differential equation via a rigorous integrator. From these computations, the monodromy matrices are derived, generating the monodromy group of the differential equation. This method establishes a mathematically rigorous framework for addressing the monodromy problem in differential equations. For a notable example, we apply our computer-assisted proof method to resolve the monodromy problem for a Picard--Fuchs differential equation associated with a family of K3 toric hypersurfaces.

Figures (2)

• Figure 1: Singular locus $\mathcal{S}$ of \ref{['eq:PicardFuchs']} (red lines) and the generic line $\bm{\ell}$ (black thick line): Four singular points $p_i$ ($i=1,\dots,4$) appear on $\bm{\ell}$, but two more points $p_5$ and $p_6$ cannot be seen in this picture because these have imaginary part. We also take the base point $p_0$ in \ref{['eq:base_pt']} on the line $\bm{\ell}$.
• Figure 2: A brief sketch of each path $\Sigma_{i}$ ($i=1,\dots,6$) of the contour: From the base point $p_0$, the solution of \ref{['eq:diff_eq']} is analytically continued to the neighborhood of each singular point via rigorous integration of ODEs. On each path, looping around the singular point, we get back to the base point.

Theorems & Definitions (24)

• Remark 1.2: Software supporting interval arithmetic and rigorous integrator of ODEs
• Remark 1.3: Monodromy without explicit fundamental system of solutions
• Theorem 1.4
• Remark 1.5
• Remark 2.1
• Remark 2.2
• Theorem 2.3: bib:ishige
• Remark 2.4
• Lemma 3.1
• Lemma 3.2