The antiderivatives $\ln x + C$ of $1/x$ live in the logarithmic extension $\mathbb{C}(x,\ln x)$

Proved

LiouvilleDiffAlg.inv_X_antideriv_logExtension

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-algebrarational-functions

Equip $\mathbb{C}(x)$ with the standard derivative $D = d/dx$ . There is a differential field extension $G \supseteq \mathbb{C}(x)$ and an element $t = \text{“}\ln x\text{”} \in G$ such that

$G = \mathbb{C}(x)(t)$ and $t$ is transcendental over $\mathbb{C}(x)$ ;
$Dt = \dfrac{Dx}{x}$ , so $G = \mathbb{C}(x, \ln x)$ is a logarithmic extension of $\mathbb{C}(x)$ ;
the antiderivatives of $1/x$ in $G$ are exactly the elements $t + C$ with $C \in \mathbb{C}$ :

Dg = \frac{1}{x} \iff g = \ln x + C \text{ for some } C \in \mathbb{C} \qquad (g \in G).

Together with the previous milestone, this shows that a logarithmic extension is needed to integrate $1/x$ .

Formalization Note The extension is packaged as an existential over a type $G$ with a field structure, a derivation, and a $\mathbb{C}(x)$ -algebra structure compatible with the derivations.

Preamble

import Mathlib
import Definitions.Def_LiouvilleDiffAlg_RatFunc

open scoped Differential

Formal statement

namespace LiouvilleDiffAlg

theorem inv_X_antideriv_logExtension [Differential (RatFunc ℂ)] (hD : IsStandardDerivation) :
    ∃ (G : Type) (_ : Field G) (_ : Differential G) (_ : Algebra (RatFunc ℂ) G)
      (_ : DifferentialAlgebra (RatFunc ℂ) G) (t : G),
      IntermediateField.adjoin (RatFunc ℂ) {t} = ⊤ ∧ Transcendental (RatFunc ℂ) t ∧
      t′ = (algebraMap (RatFunc ℂ) G RatFunc.X)′ / algebraMap (RatFunc ℂ) G RatFunc.X ∧
      ∀ g : G, g′ = algebraMap (RatFunc ℂ) G (1 / RatFunc.X) ↔
        ∃ c : ℂ, g = t + algebraMap (RatFunc ℂ) G (algebraMap ℂ (RatFunc ℂ) c) := by sorry

end LiouvilleDiffAlg

Source

Wikipedia, "Liouville's theorem (differential algebra)", revision oldid=1349223559, https://en.wikipedia.org/w/index.php?title=Liouville%27s_theorem_(differential_algebra)&oldid=1349223559, section "Examples": "Its antiderivatives

\ln x + C

do, however, exist in the logarithmic extension

\mathbb{C}(x, \ln x)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements below (Aristotle, by Harmonic), with full knowledge of the source article and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; please compare it against the Lean code yourself.

Assume $\mathbb{C}(x)$ carries a derivation $D$ (over $\mathbb{Z}$ ) with $D(p) = p'$ for all polynomials $p$ . Then there exist: a type $G$ (in the lowest universe) with a field structure, a derivation $D_G$ on $G$ , a $\mathbb{C}(x)$ -algebra structure $\iota : \mathbb{C}(x) \to G$ such that $D_G(\iota r) = \iota(Dr)$ for all $r$ , and an element $t \in G$ , such that all of the following hold:

the intermediate field generated by $t$ over $\mathbb{C}(x)$ is all of $G$ ;
$t$ is transcendental over $\mathbb{C}(x)$ ;
$D_G t = D_G(\iota x) / \iota x$ ;
for every $g \in G$ :

D_G g = \iota(1/x) \iff \exists\, c \in \mathbb{C}:\; g = t + \iota(c),

where $c$ is viewed as a constant rational function before applying $\iota$ .

Item 4 says that every antiderivative of $\iota(1/x)$ in $G$ differs from $t$ by an embedded complex number, and that every such shift is an antiderivative.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The antiderivatives ln⁡x+C\ln x + Clnx+C of 1/x1/x1/x live in the logarithmic extension C(x,ln⁡x)\mathbb{C}(x,\ln x)C(x,lnx)

The antiderivatives $\ln x + C$ of $1/x$ live in the logarithmic extension $\mathbb{C}(x,\ln x)$