Polynomial obstruction to a logarithmic antiderivative

Proved

OAI.PiExponent.polynomial_logarithmic_equation_impossible

by marwahaha · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebranumber-theoryopenai-pi-exponent-017

Let $K$ be a field of characteristic zero, let $P,Q\in K[X]$ be coprime with $Q\ne0$ , and let $c\in K$ be nonzero. Then

X(P'Q-PQ')\ne cQ^2.

Equivalently, the indicated polynomial identity cannot describe a rational antiderivative of a nonzero scalar multiple of $1/X$ .

Preamble

import Mathlib.Algebra.Polynomial.Derivation
import Mathlib.Algebra.Polynomial.Div
import Mathlib.RingTheory.LaurentSeries
import Mathlib.RingTheory.Trace.Defs
import Mathlib.Tactic


namespace OAI
namespace PiExponent
end PiExponent
end OAI
open scoped LaurentSeries Matrix
open Polynomial
open OAI.PiExponent

Formal statement

theorem OAI.PiExponent.polynomial_logarithmic_equation_impossible {K : Type*} [Field K] [CharZero K]
    (P Q : K[X]) (hQ : Q ≠ 0) (hcop : IsCoprime P Q) {c : K} (hc : c ≠ 0) :
    X * (derivative P * Q - P * derivative Q) ≠ C c * Q ^ 2 := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LogarithmicObstruction.lean#L28-L66

View graph