Algebraic polynomial interpolation of cleared derivative rows

Proved

ArithmeticE.cleared_derivative_jet_interpolation

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

differential-equationsformalizationlinear-algebra

Let $T\in\mathbb Q[X]$ and let $B$ be an $m\times m$ rational polynomial matrix. Fix an algebraic complex number $\xi$ with $T(\xi)\ne0$ . For any $N\ge0$ and any prescribed algebraic rows $w_0,\ldots,w_{N-1}\in\overline{\mathbb Q}^{\,m}$ , there is a row $P$ of polynomials with algebraic coefficients such that

R_k(P)(\xi)=w_k\qquad(0\le k<N),

where $R_0(P)=P$ and $R_{k+1}(P)=TR_k(P)'+R_k(P)B-kT'R_k(P)$ .

This is the finite interpolation component of the ordinary cyclic-vector construction. It involves no E-functions, convergence, or arithmetic denominator estimates. The cases $N=0$ and $m=0$ are included.

Preamble

import Definitions.Def_clearedDerivativeRows
open ArithmeticE

Formal statement

theorem ArithmeticE.cleared_derivative_jet_interpolation
    (m : ℕ) (T : Polynomial ℚ) (B : Matrix (Fin m) (Fin m) (Polynomial ℚ))
    (ξ : ℂ) (hξ : IsAlgebraic ℚ ξ)
    (hreg : T.eval₂ (algebraMap ℚ ℂ) ξ ≠ 0)
    (N : ℕ) (w : ℕ → Fin m → ℂ)
    (hw : ∀ k < N, ∀ i, IsAlgebraic ℚ (w k i)) :
    ∃ P : Fin m → Polynomial ℂ,
      (∀ i k, IsAlgebraic ℚ ((P i).coeff k)) ∧
      ∀ k < N, ∀ i, (clearedDerivativeRows T B P k i).eval ξ = w k i := 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