The Taub-NUT Metric Is Not Projectively Induced
Shaosai Huang
math.DG
Sep 18, 2026 · v1
TL;DR
The analytic core of the proof, plus a Weyl–Papapetrou form computation, is machine-checked in Lean 4.
Abstract
LeBrun's Kähler realization $g_m$ of the Taub–NUT metric on $\mathbb{C}^2$ is complete, Ricci-flat and not flat. Loi, Zedda and Zuddas proved that no multiple $αg_m$ admits a Kähler immersion into a finite- or infinite-dimensional complex projective space when $m>α/2$, and conjectured that the same holds for every $m>0$. We prove the conjecture. The restriction of the Kähler potential to the axis $z_2=0$ is governed by the Lambert $W$ function, so $\exp(αΦ_m)$ has a finite radius of convergence as a power series in $|z_1|^2$ although it is real analytic on the whole half-line; the Vivanti–Pringsheim theorem forbids nonnegative Taylor coefficients, and Calabi's criterion fails. We state the mechanism, which Arezzo, Loi, Placini and Zedda recently used for radial metrics, as a general obstruction to Kähler immersions. In statistical terms the axis restriction of $g_m$ would be a natural exponential family with mean domain $(0,\infty)$ and variance function $μ/(1+2mμ)$; the argument gives an elementary proof of the known fact, due to Bar-Lev, Bshouty and Enis, that no such family exists with variance function $μ/(1+cμ)$ for any $c>0$. The result confirms onemore case of the conjecture of Loi, Salis and Zuddas that Ricci-flat projectively induced Kähler metrics are flat. The analytic core of the proof has been machine-checked in Lean 4.
Problem
LeBrun's Kähler realization of the Taub–NUT metric on C^2 is complete, Ricci-flat and non-flat. Loi, Zedda and Zuddas conjectured that no multiple of it admits a Kähler immersion into finite- or infinite-dimensional complex projective space for every m>0.
Approach
The restriction of the Kähler potential to the axis is expressed through the Lambert W function, giving a power series with finite radius of convergence that is nevertheless real analytic on the whole half-line. Calabi's criterion converts existence of a Kähler immersion into positivity of Taylor coefficients, and the Vivanti–Pringsheim theorem forbids nonnegative coefficients with a finite radius, yielding a contradiction. The analytic core of the argument was checked in Lean 4, and the Weyl–Papapetrou / Gibbons–Hawking form of the metric was verified in Lean and an ancillary script.
Results
The conjecture is proven: no multiple of the Taub–NUT metric admits a Kähler immersion into complex projective space for any m>0. This confirms one more case of the Loi–Salis–Zuddas conjecture that Ricci-flat projectively induced Kähler metrics are flat, and gives an elementary proof of a related nonexistence result for exponential families.
