Squeezing self-intersections from section dimensions

Let $S,T$ be surfaces with $L$ ample on $S$, $D$ ample on $T$, and $k,r\in\mathbb N$. If for all $n$ one has $h^0(T,D^n)\le h^0(S,L^{kn})$ and $2h^0(S,L^{kn})\le 2h^0(T,D^n)+rn(n+1)$, then $k^2L^2-r\le D^2\le k^2L^2$.

Notation. $L^2$ is selfIntersection, namely $\chi(L^2)-2\chi(L)+\chi(\mathcal O_S)$. $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$.

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.