English
For an affine Weierstrass curve W' over a commutative ring R and for elements x, y, ℓ in R, the x-coordinate polynomial of the sum is determined by a quadratic relation involving the line through the two points and the negation polynomial of the curve.
Русский
Для аффинной кривой Вейерштрасса W' над коммутативной кольцом R и элементов x, y, ℓ в R координатный полином суммы задаётся через линейное пересечение (прямую) и полином-одиночку кривой; тождество выражает взаимосвязь координат суммы через эти объекты.
LaTeX
$$$ C\bigl(W'.addPolynomial(x,y,\ell)\bigr) = \bigl(Y - C\bigl(\mathrm{linePolynomial}(x,y,\ell)\bigr)\bigr) \cdot \bigl(W'.negPolynomial - C\bigl(\mathrm{linePolynomial}(x,y,\ell)\bigr)\bigr) + W'.polynomial $$$
Lean4
theorem C_addPolynomial (x y ℓ : R) :
C (W'.addPolynomial x y ℓ) =
(Y - C (linePolynomial x y ℓ)) * (W'.negPolynomial - C (linePolynomial x y ℓ)) + W'.polynomial :=
by
rw [addPolynomial, linePolynomial, polynomial, negPolynomial]
eval_simp
C_simp
ring1
