A regular derivative-coordinate matrix yields a minimal scalar equation

Proved

ArithmeticE.polynomial_derivative_frame_minimal_equation

by shivm · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-equationsformalizationlinear-algebra

Let $F\in\mathbb C[[X]]$ , $\xi\in\mathbb C$ , and $n\ge0$ . Suppose $F$ has a polynomial derivative frame of order $n$ : there are polynomially independent series $g_j$ and polynomial data $d,A,b$ with

dF^{(i)}=\sum_j A_{ij}g_j\quad(i<n),\qquad dF^{(n)}=\sum_j b_jg_j,

and $d(\xi)(\det A)(\xi)\ne0$ . Then there are polynomials $p_k$ such that

\sum_{k=0}^n p_kF^{(k)}=0,\qquad p_n(\xi)\ne0,

and no nonzero polynomial differential operator of order less than $n$ annihilates $F$ .

Thus the equation has minimal order and is ordinary at $\xi$ . This is a purely algebraic implication; it has no E-function or arithmetic hypothesis. Order zero is allowed and corresponds to the frame forcing $F=0$ .

Preamble

import Definitions.Def_polynomialDerivativeFrame
open ArithmeticE

Formal statement

theorem ArithmeticE.polynomial_derivative_frame_minimal_equation
    (F : PowerSeries ℂ) (ξ : ℂ) (n : ℕ)
    (hf : PolynomialDerivativeFrame F ξ n) :
    ∃ p : ℕ → Polynomial ℂ, MinimalEquation p n F ∧ (p n).eval ξ ≠ 0 := by sorry

Source

Auxiliary formalization of Beukers, A refined version of the Siegel–Shidlovskii theorem, Theorem 3.2, printed pp. 6–7 (prescribed derivative rows and determinant equation), https://webspace.science.uu.nl/~beuke106/siegelshidlovskii.pdf. These explicit polynomial-numerator and module-coordinate interfaces are derived from the proof, not quoted named lemmas.

View graph