English
There is a detailed homogeneous identity for negAddY(P,Q) equating it to a combination of products of (P0, P1, P2) and (Q0, Q1, Q2) with the Weierstrass coefficients.
Русский
Существует детальное однородное тождество для negAddY(P,Q), выражающее его через комбинацию произведений координат P и Q с коэффициентами кривой.
LaTeX
$$$W'.negAddY(P,Q) \; = \; \text{(long homogeneous polynomial in }P_i,Q_i,a_j) / (P_z Q_z)^2$$$
Lean4
theorem negAddY_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
W'.negAddY P Q * (P z * Q z) ^ 2 =
(P y * Q z - Q y * P z) *
((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 * (P x * Q z - Q x * P z) ^ 2) +
P y * Q z * (P x * Q z - Q x * P z) ^ 3 :=
by
linear_combination (norm := (rw [negAddY]; ring1))
(2 * Q y * P z * Q z ^ 3 - P y * Q z ^ 4) * (equation_iff _).mp hP +
(Q y * P z ^ 4 - 2 * P y * P z ^ 3 * Q z) * (equation_iff _).mp hQ
