Comparing H^2 across a section of a generated bundle

Let $S$ be a surface with ample $A$, $L,M$ line bundles, $s$ a finite family of sections of $L$ with iso-opens covering $S$, $v$ a coefficient vector with nonzero combination, and suppose the section ideal defines an integral curve $C$ of dimension one with $\deg_C(L\otimes M)\ge0$. Then $h^2(S,M)\le h^1(C,\mathcal O_C)+h^2(S,L\otimes M)$.

Notation. $\deg_CL$ is curveDegree, namely $\chi(L|_C)-\chi(\mathcal O_C)$. $h^n$ is cohomologyDimension, the Module.finrank over $\mathbb C$ of $\operatorname{Ext}^n(\mathcal O,-)$, which is 0 for an infinite-dimensional space. 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$. An IntegralCurve on a surface is an integral closed subscheme of topological Krull dimension one, given by a closed immersion.

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.