English
For P, Q on a Weierstrass curve W′ over a ring R, the product addX(P,Q)·(Pz Qz)^2 equals the product of a certain polynomial in the coordinates of P and Q by (Px Qz − Qx Pz).
Русский
Для точек P, Q на кривой Вейершстраса W′ над кольцом R произведение addX(P,Q) на (Pz Qz)^2 равно произведению некоторого многочлена от координат P и Q на (Px Qz − Qx Pz).
LaTeX
$$$W'.addX(P,Q) \cdot (P_z Q_z)^2 = \Big( (P_y Q_z - Q_y P_z)^2 P_z Q_z + a_1 (P_y Q_z - Q_y P_z) P_z Q_z (P_x Q_z - Q_x P_z) - a_2 P_z Q_z (P_x Q_z - Q_x P_z)^2 - P_x Q_z (P_x Q_z - Q_x P_z)^2 - Q_x P_z (P_x Q_z - Q_x P_z)^2 \Big) \cdot (P_x Q_z - Q_x P_z),$$
Lean4
theorem addX_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
W'.addX P Q * (P z * Q z) ^ 2 =
((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
(P x * Q z - Q x * P z) :=
by
linear_combination (norm := (rw [addX]; ring1))
(2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) * (equation_iff _).mp hP +
(Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) * (equation_iff _).mp hQ
