Constructing Rational Curves via Jets on Projective Varieties with Non-Nef Canonical Bundle
Bin Dong, Guoxiong Gao, Bin Guo, Zeming Sun, Bin Wu, Song-Yan Xie
math.AG
Sep 23, 2026 · v1
math.CV
TL;DR
Main arguments of the algebraic Miyaoka–Mori criterion proof were formalized in Lean 4, reported in an appendix.
Abstract
We give an algebraic proof in characteristic zero of the Miyaoka–Mori criterion: every point of a curve of negative canonical degree on a smooth projective variety lies on a rational curve. Our jet technique gives, in addition, an effective numerical decomposition of the original curve class. For each prescribed point, the decomposition contains a rational curve through that point, with a positive coefficient independent of the point and with anticanonical degree at most $\dim X+1$. Together with BDPP cone duality, this recovers the projective uniruledness criterion over $\mathbb C$. The main result of this paper was obtained using the Pharos system. A detailed report on the use of Pharos and on the Lean 4 formalization of the main arguments is given in the Appendix B, written by Bin Dong, Guoxiong Gao, Zeming Sun, and Bin Wu.
Problem
The Miyaoka–Mori criterion states that every point of a curve of negative canonical degree on a smooth projective variety lies on a rational curve. The classical proof relies on Frobenius amplification in positive characteristic; an algebraic characteristic-zero proof was sought.
Approach
Weighted jets replace Frobenius amplification, producing a ruled surface whose fibers give rational curves through points of the given curve. A twisted affine cone and inverse tautological class are used to construct polynomial realizations. The main result was obtained using the Pharos system, with the main arguments formalized in Lean 4.
Results
An algebraic characteristic-zero proof of the Miyaoka–Mori criterion is given, together with an effective numerical decomposition of the curve class, yielding a rational curve through each prescribed point with anticanonical degree at most dim X + 1. Combined with BDPP cone duality, this recovers the projective uniruledness criterion over the complex numbers.
