{"id":"palomar/PALOMAR-2026-10-30-000004","url":"https://github.com/tdupu/pcfawd-formalization/tree/05890ba0b0453c289157df45c5bbe472551b1025/char-zero/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-30-000004-v1.json","repo":"https://github.com/tdupu/pcfawd-formalization","tags":["math.DS","math.AG","math.NT","msc:37P55","msc:14E22"],"score":0,"title":"PCF all the way down","trust":"high","domain":"math.DS","source":"palomar","authors":["Taylor Dupuy","Thomas Tucker","Zhuoran Wang"],"reviews":0,"subject":"math.DS","summary":"Let k be a field of characteristic zero and let f: X → X be a finite surjective map of integral k-schemes of finite type. By the critical locus of f we mean the image in X of the critical locus of the map induced on the normalization of X. By the branch locus we mean the image of the critical locus under f. We say that f is post-critically finite (PCF) if, for every irreducible divisor D contained in the branch locus, the forward orbit f(D) ∪ f^2(D) ∪ … is algebraic, that is, a finite union of subvarieties, taken as a closed subscheme with its reduced induced structure. We prove that if f is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-30","reactions":{},"formalized":true,"formalizes":[{"title":"PCF all the way down","identifier":"","relationship":"adapts"}]}