All.lean

Branched coverings of the projective line over the integers

Formalization of Ryoji Shimizu and Naganori Yamaguchi's On branched coverings of the projective line over the integers, using the numbering of arXiv v1. Numbered files contain the corresponding paper arguments; Arithmetic and Geometry contain their supporting constructions.

Includes section intersection calculations for Lemma 2.3, the dyadic collision calculation for Lemma 2.4, the quadratic quotient construction for Proposition 2.5, and the case of at least seven sections in Corollary 2.7. The full finite-divisor normal-crossing criterion and its comparison over Z_p, the remaining geometric hypotheses of the paper statements, and the main quotient criteria remain outside the completed formalization. Existing boundary and solvable-covering results are reused from Yamaguchi26SolvableCoverings as their concrete hypotheses are supplied.