Sections of coprime degree with integral zero loci

Let $L$ be ample on a surface $S$ and $a>0$. There are $b>0$ coprime to $a$, a finite family $s$ of sections of $L^b$ with iso-opens covering $S$, and coefficients $v\in\mathbb C$, such that the combination is nonzero and its section ideal defines an integral subscheme of dimension one.

Notation. The iso-open of $s$ (SectionOpens.isoOpen s) is the union of the opens on which the morphism $s$ restricts to an isomorphism. sectionIdeal k s hs v is the comap along sectionsMorphism of the ideal sheaf of the hyperplane with coefficients $v$; sectionCombination k s v is $\sum_j k(v_j)s_j$. IsAmple means that for each point $x$ and open $V\ni x$, some positive power has a global section with nonvanishing open containing $x$, inside $V$, and affine. A Surface is an integral scheme smooth of relative dimension 2 over $\operatorname{Spec}\mathbb C$ with a closed immersion into some complex projective space over $\mathbb C$.

Formalization Note The statement is verbatim from OpenAI's Lean development, with Definitions files of this development imported in place of the upstream modules; these are supporting code for the statement.