English
The Y-coordinate of the negative P+Q, negAddY(P,Q), is given by a polynomial expression in the coordinates of P and Q, together with the Weierstrass coefficients.
Русский
Y-координата вершины -(P+Q) задаётся полиномом по координатам P и Q и коэффициентам Вейерштрасс.
LaTeX
$$W'.negAddY P Q * (P z ^ 3 Q z ^ 3) = (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$$
Lean4
/-- The `Y`-coordinate of a representative of `-(P + Q)` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.
If the representatives of `P` and `Q` are equal, then this returns the value `0`. -/
def negAddY (P Q : Fin 3 → R) : R :=
-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
P x ^ 3 * Q y * Q z ^ 3 -
2 * P y ^ 2 * Q y * Q z ^ 3 +
W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
W'.a₃ * Q y ^ 2 * P z ^ 6 -
W'.a₃ * P y ^ 2 * Q z ^ 6 -
W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
W'.a₄ * P x * P y * P z * Q z ^ 6 -
2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6
