Quartics smooth and integral away from the centre

For $L$ ample on $S$ there are $d>0$, $N,n$, sections $s$ of $L^d$ indexed by $\operatorname{Option}(\operatorname{Fin}N)$ with iso-opens covering $S$, an equivalence $e$, and $y$ such that $y$ is the only point outside centeredOpen s, the sections define a closed immersion, and for each nonzero $P$ there is $v$ with $P(v)\ne0$ such that the comap to the centered open of doublePointQuarticIdeal k s hs (v ∘ e.symm) has integral subscheme, smooth over $\mathbb C$.

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)$. 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$. centeredOpen s is the union of the iso-opens of $s_{\mathrm{some}\,i}$. QuarticIndex σ is $\sigma\times\sigma\times\operatorname{Option}\sigma\times\operatorname{Option}\sigma$; doublePointQuartics are the corresponding degree-4 mixed products of the sections.

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.