PCF All The Way Down

Taylor Dupuy, Alon Levy, Thomas Tucker, Zhuoran Wang

math.AG Nov 4, 2026 · v2 math.DS math.NT

Read PDF arXiv abstract

TL;DR

The main theorem and a corollary on post-critically finite maps are formalized in Lean 4 against Mathlib, with a public repository and blueprint.

Abstract

We prove that a finite surjective post-critically finite self-map of a variety in characteristic zero remains post-critically finite on every preperiodic integral effective divisor after passing to its periodic image with its return map. Iterating this result proves PCF all the way down. A detailed report on AI usage is contained in the manuscript.

Problem

The question is whether a finite surjective post-critically finite (PCF) self-map of a characteristic-zero variety stays PCF when restricted to preperiodic integral effective divisors, after passing to the periodic image with its return map.

Approach

The authors prove the restriction property and iterate it to obtain 'PCF all the way down'. AI models assisted with the bounding argument, counterexamples, source checks, drafting, and the Lean formalization. Theorem 1.1 and Corollary 8.2 are formalized in Lean 4 (v4.35.0) against Mathlib, using integral, locally finite type Noetherian schemes. A blueprint maps the paper's claims to Lean declarations.

Results

The main theorem and its corollary are machine-checked in Lean 4. A public repository provides the code and a statement-to-declaration map.

Papers With

PCF All The Way Down