H^1 comparison on an integral curve

Let $C$ be an integral curve on a surface $S$ with an ample $A$, and $M$ a line bundle on $C$ with $\chi(M)-\chi(\mathcal O_C)\ge0$. Then $h^1(C,M)\le h^1(C,\mathcal O_C)$.

Notation. $\chi$ is eulerCharacteristic: the alternating sum of $\mathbb C$-dimensions of $\operatorname{Ext}^n(\mathcal O,-)$, for $n\le2$ on a surface and $n\le1$ on a curve. $h^n$ is cohomologyDimension, the Module.finrank over $\mathbb C$ of $\operatorname{Ext}^n(\mathcal O,-)$, which is 0 for an infinite-dimensional space. 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.