/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilLam--Litt conjecture
A conjecture of Lam and Litt on algebraic solutions of algebraic ODEs.
Let $g \in \mathbb{Q}(z, y_0, \dots, y_{n-1})$ be a rational function in $n + 1$ variables. Let $f$ be a power series over $\mathbb{Q}$ such that $f^{(n)}(z) = g(z, f(z), f'(z), \dots, f^{(n-1)}(z))$. Also, assume that $g(0, f(0), f'(0), \dots, f^{(n-1)}(0))$ is defined. Then the following are equivalent:
$f$ is algebraic over $\mathbb{Q}[z]$.
There exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$.
There exists an integer-valued function $\omega$ on the set of primes with $\lim_{p \to \infty} \omega(p) / p = \infty$ such that, for each prime $p$, the rational numbers $a_0, a_1, \dots, a_{\omega(p)}$ are in $\mathbb{Z}_{(p)}$.
The implication 1) => 2) is due to Eisenstein, and 2) => 3) is trivial.
References:
Yeuk Hay Joshua Lam, Daniel Litt, "Algebraicity and integrality of solutions to differential equations", arxiv/2501.13175
Gotthold Eisenstein. "Über eine allgemeine Eigenschaft der Reihen-Entwicklungen aller algebraischen Funktionen", Bericht der Königl. Preuss. Akademie der Wissenschaften zu Berlin, 1852
TODO:
Lam-Litt conjecture implies Grothendieck p-curvature conjecture.
Examples in Remark 1.1.3 and 1.1.5 on the conditions of the conjecture.
open Real MvPolynomial PowerSeriesnamespace LamLitt
A power series $f$ is a solution of an algebraic ODE defined by the rational function
$g \in \mathbb{Q}(z, y_0, \dots, y_{n-1})$ if $f^{(n)}(z) = g(z, f(z), f'(z), \dots, f^{(n-1)}(z))$.
The variable indexed by 0 : Fin (n + 1) corresponds to $z$, and the variable indexed by
i.succ corresponds to $y_i = f^{(i)}(z)$.
def IsSolutionOfAlgebraicODE (n : ℕ) (f : PowerSeries ℚ) (g : MvRatFunc (Fin (n + 1)) ℚ) : Prop :=
let pt : Fin (n + 1) → PowerSeries ℚ := Fin.cases X (fun i : Fin n ↦ (derivative ℚ)^[i.val] f)
∃ p q : MvPolynomial (Fin (n + 1)) ℚ,
q ≠ 0 ∧
g = (algebraMap _ _ p) / (algebraMap _ _ q) ∧
IsDefined (Fin (n + 1)) ℚ g (PowerSeries.constantCoeff ∘ pt) ∧
(derivative ℚ)^[n] f * MvPolynomial.aeval pt q = MvPolynomial.aeval pt pdef ℤAdjoinInvNat (N : ℕ) : Subalgebra ℤ ℚ := Algebra.adjoin ℤ {(1 / N : ℚ)}There exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$.
def IsCoeffIntegralAdjointInvNat (f : PowerSeries ℚ) (N : ℕ) : Prop :=
∀ n : ℕ, coeff n f ∈ ℤAdjoinInvNat NFor an integer-valued function $\omega$ on the set of primes and a sequence $a_n$ of rational numbers, the condition $\omega$-integrality means that for each prime $p$, the rational numbers $a_0, a_1, \dots, a_{\omega(p)}$ are in $\mathbb{Z}_{(p)}$, i.e. their denominators are not divisible by $p$. When $\omega(p) < 0$ the constraint at $p$ is vacuous.
def omegaIntegral (ω : Nat.Primes → ℤ) (a : ℕ → ℚ) : Prop :=
∀ p : Nat.Primes, ∀ j : ℕ, (j : ℤ) ≤ ω p → Nat.Coprime (a j).den p
The growth condition on $\omega$: the ratio $\omega(p) / p$ tends to infinity as the prime $p$
tends to infinity, i.e. $\lim_{p \to \infty} \omega(p) / p = \infty$. Here the source filter is
Filter.atTop on the primes, obtained by pulling back Filter.atTop on $\mathbb{N}$ along the
coercion Nat.Primes → ℕ.
def omegaSuperlinear (ω : Nat.Primes → ℤ) : Prop :=
Filter.Tendsto (fun p : Nat.Primes ↦ (ω p : ℝ) / p)
(Filter.comap (fun p : Nat.Primes ↦ (p : ℕ)) Filter.atTop) Filter.atTopEisenstein's theorem (1852): an algebraic power series over $\mathbb{Q}[z]$ has bounded denominators, i.e., there exists $N$ such that all coefficients lie in $\mathbb{Z}[1/N]$.
@[category research solved, AMS 12 13]
theorem lam_litt.variants.eisenstein (f : PowerSeries ℚ) (hAlg : IsAlgebraic (Polynomial ℚ) f) :
∃ N : ℕ, IsCoeffIntegralAdjointInvNat f N := f:ℚ⟦X⟧hAlg:IsAlgebraic (Polynomial ℚ) f⊢ ∃ N, IsCoeffIntegralAdjointInvNat f N
All goals completed! 🐙Every element of $\mathbb{Z}[1/N]$ has denominator coprime to any prime $p$ not in the prime factor set of $N$ (vacuously, the case $N = 0$ gives $\mathbb{Z}[1/N] = \mathbb{Z}$).
N:ℕp:ℕhp:Nat.Prime phpN:p ∉ N.primeFactorsq:ℚhN:N ≠ 0⊢ N.Coprime p
All goals completed! 🐙
N:ℕp:ℕhp:Nat.Prime phpN:p ∉ N.primeFactorsq:ℚr✝:ℤ⊢ ((algebraMap ℤ ℚ) r✝).den.Coprime p All goals completed! 🐙
N:ℕp:ℕhp:Nat.Prime phpN:p ∉ N.primeFactorsq:ℚx✝:ℚy✝:ℚhx✝:x✝ ∈ ℤ[1 / ↑N]hy✝:y✝ ∈ ℤ[1 / ↑N]ihx:x✝.den.Coprime pihy:y✝.den.Coprime p⊢ (x✝ + y✝).den.Coprime p All goals completed! 🐙
N:ℕp:ℕhp:Nat.Prime phpN:p ∉ N.primeFactorsq:ℚx✝:ℚy✝:ℚhx✝:x✝ ∈ ℤ[1 / ↑N]hy✝:y✝ ∈ ℤ[1 / ↑N]ihx:x✝.den.Coprime pihy:y✝.den.Coprime p⊢ (x✝ * y✝).den.Coprime p All goals completed! 🐙Textbook implication: integrality (2) trivially implies ω(p)-integrality (3).
@[category textbook, AMS 12]
theorem lam_litt.variants.integrality_implies_omega_integrality
(f : PowerSeries ℚ) (N : ℕ) (hN : IsCoeffIntegralAdjointInvNat f N) :
∃ ω : Nat.Primes → ℤ, omegaSuperlinear ω ∧ omegaIntegral ω (PowerSeries.coeff · f) := f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ ∃ ω, omegaSuperlinear ω ∧ omegaIntegral ω fun x ↦ (PowerSeries.coeff x) f
-- Take ω(p) = -1 if p divides N, else p^2.
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ omegaSuperlinear fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ omegaIntegral (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) fun x ↦ (PowerSeries.coeff x) f
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ omegaSuperlinear fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2 f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ (Nat.cast ∘ fun p ↦ ↑p) =ᶠ[Filter.comap (fun p ↦ ↑p) Filter.atTop] fun p ↦
↑((fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) p) / ↑↑p
filter_upwards [(Filter.eventually_gt_atTop N).comap ((↑) : Nat.Primes → ℕ)] with p f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.PrimeshpN_lt:p ∈ {x | N < ↑x}⊢ (Nat.cast ∘ fun p ↦ ↑p) p = ↑(if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) / ↑↑p
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.PrimeshpN_lt:p ∈ {x | N < ↑x}hpN:↑p ∉ N.primeFactors⊢ (Nat.cast ∘ fun p ↦ ↑p) p = ↑(if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) / ↑↑p
All goals completed! 🐙
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ omegaIntegral (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) fun x ↦ (PowerSeries.coeff x) f f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.Primesj:ℕhj:↑j ≤ (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) p⊢ ((fun x ↦ (PowerSeries.coeff x) f) j).den.Coprime ↑p
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.Primesj:ℕhj:↑j ≤ (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) phpmem:↑p ∈ N.primeFactors⊢ ((fun x ↦ (PowerSeries.coeff x) f) j).den.Coprime ↑pf:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.Primesj:ℕhj:↑j ≤ (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) phpmem:↑p ∉ N.primeFactors⊢ ((fun x ↦ (PowerSeries.coeff x) f) j).den.Coprime ↑p
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.Primesj:ℕhj:↑j ≤ (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) phpmem:↑p ∈ N.primeFactors⊢ ((fun x ↦ (PowerSeries.coeff x) f) j).den.Coprime ↑p f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.Primesj:ℕhpmem:↑p ∈ N.primeFactorshj:↑j ≤ -1⊢ ((fun x ↦ (PowerSeries.coeff x) f) j).den.Coprime ↑p; All goals completed! 🐙
f:ℚ⟦X⟧N:ℕhN:IsCoeffIntegralAdjointInvNat f Np:Nat.Primesj:ℕhj:↑j ≤ (fun p ↦ if ↑p ∈ N.primeFactors then -1 else ↑↑p ^ 2) phpmem:↑p ∉ N.primeFactors⊢ ((fun x ↦ (PowerSeries.coeff x) f) j).den.Coprime ↑p All goals completed! 🐙implies 2): if the coefficients of $f$ satisfy the $\omega$-integrality condition for some superlinear $\omega$, then there exists $N$ such that for all $n$, the $n$-th coefficient of $f$ is in $\mathbb{Z}[1/N]$.
@[category research open, AMS 11 14]
theorem lam_litt.variants.omega_integrality_implies_algebraicity {n : ℕ} (f : PowerSeries ℚ)
(g : MvRatFunc (Fin (n + 1)) ℚ) (hODE : IsSolutionOfAlgebraicODE n f g)
(ω : Nat.Primes → ℤ) (hω : omegaSuperlinear ω ∧ omegaIntegral ω (PowerSeries.coeff · f)) :
∃ N : ℕ, IsCoeffIntegralAdjointInvNat f N := n:ℕf:ℚ⟦X⟧g:MvRatFunc (Fin (n + 1)) ℚhODE:IsSolutionOfAlgebraicODE n f gω:Nat.Primes → ℤhω:omegaSuperlinear ω ∧ omegaIntegral ω fun x ↦ (PowerSeries.coeff x) f⊢ ∃ N, IsCoeffIntegralAdjointInvNat f N
All goals completed! 🐙implies 1): if the coefficients of $f$ are in $\mathbb{Z}[1/N]$ for some $N$, then $f$ is algebraic over $\mathbb{Q}[z]$. Also the version of conjecture of Litt's problem 1 on his website.
@[category research open, AMS 11 14]
theorem lam_litt.variants.integrality_implies_algebraicity {n : ℕ} (f : PowerSeries ℚ)
(g : MvRatFunc (Fin (n + 1)) ℚ) (hODE : IsSolutionOfAlgebraicODE n f g)
(N : ℕ) (hN : IsCoeffIntegralAdjointInvNat f N) :
IsAlgebraic (Polynomial ℚ) f := n:ℕf:ℚ⟦X⟧g:MvRatFunc (Fin (n + 1)) ℚhODE:IsSolutionOfAlgebraicODE n f gN:ℕhN:IsCoeffIntegralAdjointInvNat f N⊢ IsAlgebraic (Polynomial ℚ) f
All goals completed! 🐙end LamLitt