Lange geometric construction of a local quadratic addition cover

Let $K$ be algebraically closed of characteristic zero and let $E$ be a connected commutative algebraic group. There is a projective realization $F\subseteq\mathbf P^N$ and a group isomorphism $E\to F$ regular in both directions, such that every pair $(x,y)\in F\times F$ has an open neighborhood $U$ with a bihomogeneous polynomial tuple $P=(P_0,\ldots,P_N)$ of common bidegree $(d_0,d_1)$ satisfying

The first coordinate block is the point being translated. There is no asserted bound on the second-block degree, and different neighborhoods may use different tuples and degrees. This is the local geometric construction underlying quadratic addition laws.

Formalization Note. The open neighborhoods use the induced multiprojective polynomial Zariski topology on the algebraic pair variety. This formulation restricts Rovelli's local-formula conclusion to the group inside its completion and reorders the coordinate blocks. It imposes neither global compatibility outside $U$ nor an extra irreducibility hypothesis. Zero-dimensional groups are included. Constructing the reembedding and its local tuples in the existing embedded-group interface remains Open.

Verified homogenization reduction. The accepted sketch explicitly pads each affine monomial with powers of the chosen chart coordinates, producing a common bihomogeneous degree $(2,B)$. It proves that normalized evaluation is unchanged and that arbitrary nonzero chart lifts multiply the whole output tuple by one common nonzero scalar. The tuple therefore remains nonzero and represents the same sum.

The sole Open dependency is Lange reembedding with local affine quadratic addition formulas. It supplies the reembedding, coordinate-chart neighborhoods, and affine formulas quadratic in the first block. No homogeneous or common-degree condition is assumed there. The geometric construction remains Open; the algebraic passage from affine to bihomogeneous formulas is proved.