English
Let P and Q be points represented in coordinates (x, y, z) on a Weierstrass Jacobian curve, with z-coordinates nonzero. The y-coordinate of the sum P ⊖ Q has a closed form given by a rational expression in the coordinates P_x, P_y, P_z, Q_x, Q_y, Q_z involving the curve operations addX and addZ. In particular, W.negAddY(P, Q) equals the displayed rational combination of these coordinates divided by (P_z Q_z)^3.
Русский
Пусть P и Q — точки на кривой Якобиана Вейерштрасса, заданные координатами (x, y, z) с z ≠ 0. y-координата суммы P и Q имеет замкнутую форму как рациональное выражение от координат P_x, P_y, P_z, Q_x, Q_y, Q_z, используя операции кривой addX и addZ. В частности, W.negAddY(P, Q) равняется указанной рациональной комбинации координат, делённой на (P_z Q_z)^3.
LaTeX
$$$W.negAddY(P,Q) = \frac{(P_y Q_z^3 - Q_y P_z^3) \cdot (W.addX(P,Q) \cdot (P_z Q_z)^2 - P_x Q_z^2 \cdot addZ(P,Q)^2) + P_y Q_z^3 \cdot addZ(P,Q)^3}{(P_z Q_z)^3}$, where P_z \neq 0, Q_z \neq 0.$$
Lean4
theorem negAddY_eq {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
W.negAddY P Q =
((P y * Q z ^ 3 - Q y * P z ^ 3) * (W.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2) +
P y * Q z ^ 3 * addZ P Q ^ 3) /
(P z * Q z) ^ 3 :=
by rw [← negAddY_eq', mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
