Finiteness of the toric H^1 quotient for a plane cover

Let $K$ be a field, $k:K\to\Gamma(X,\top)$, and $s=(s_0,s_1,s_2)$ sections of a module $M$ with iso-opens covering $X$ such that sectionsMorphism k s hs to the plane is finite. For a line bundle $L$, the quotient of cycles by vertexBoundaries of the edge submodules planePair and vertex submodules planeVertex inside the sections over the triple overlap is finite-dimensional over $K$.

Notation. The iso-open of $s$ (SectionOpens.isoOpen s) is the union of the opens on which the morphism $s$ restricts to an isomorphism. sectionsMorphism k s hs is the morphism from $X$ to $\operatorname{Proj}$ of the graded polynomial ring in variables indexed by the sections, defined by sections whose iso-opens cover $X$, with $k$ the ring map from the base into $\Gamma(X,\top)$. cycles A B C is the submodule of $A\times B\times C$ of triples with zero sum. planeVertex and planePair are the images in the sections over the triple overlap (planeTriple) of sections over the chart of $s_i$, and over the overlap of the charts of $s_i,s_j$, respectively.

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.