English
Let P and Q be three-coordinate points on a Weierstrass Jacobian, lying on the curve, with the relation P_x Q_z^2 = Q_x P_z^2. Then the Y-coordinate derived from negAddY satisfies a cube relation with the Z-coordinates: W'.negAddY(P,Q) · (P_z Q_z)^3 = (−(P_y Q_z^3 − Q_y P_z^3))^3.
Русский
Пусть P и Q — трикомпонентные представителя точек на кривой Вейерштрасса, принадлежащие к кривой через Якобиан, и выполняется соотношение P_x Q_z^2 = Q_x P_z^2. Тогда Y-координата, полученная из функции negAddY, удовлетворяет кубической связи с Z-координатами: W'.negAddY(P,Q) · (P_z Q_z)^3 = (−(P_y Q_z^3 − Q_y P_z^3))^3.
LaTeX
$$$$ W'.\\negAddY(P,Q) \\cdot (P_z Q_z)^3 = \\big( -(P_y Q_z^3 - Q_y P_z^3) \\big)^3 $$$$
Lean4
theorem negAddY_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
(hx : P x * Q z ^ 2 = Q x * P z ^ 2) : W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3 :=
by
rw [negAddY_eq', addX_eq' hP hQ, addZ_of_X_eq hx]
ring1
