English
Under the hypotheses that the two points (x1, y1) and (x2, y2) lie on the Weierstrass curve and with a nondegeneracy condition, the constant term corresponding to the addition polynomial with slope equals a signed product of X-classes and the X-coordinate of the sum.
Русский
При условии, что точки (x1, y1) и (x2, y2) лежат на кривой Вейерштрасса и при некоррецидирующем условии, константный член полинома сложения на основе наклона равен приведённому знаковому произведению X-классов и x-координаты суммы.
LaTeX
$$$mk\,W\Big(C\big(W'.addPolynomial\ x_1\ y_1\ (W'.slope\ x_1\ x_2\ y_1\ y_2)\big)\Big) = -\big(XClass W\ x_1 \cdot XClass W\ x_2 \cdot XClass W\Big(W'.addX\ x_1\ x_2\ (W'.slope\ x_1\ x_2\ y_1\ y_2)\Big)\big)$$$
Lean4
theorem C_addPolynomial_slope [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
mk W (C <| W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
-(XClass W x₁ * XClass W x₂ * XClass W (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)) :=
congr_arg (mk W) <| W.C_addPolynomial_slope h₁ h₂ hxy
