English
The negative of P+Q in Y-coordinate, negAddY(P,Q), satisfies a homogeneous polynomial identity relating to the original addX/negAddY expressions with Weierstrass coefficients a1, a2, a3, a4, a6.
Русский
Y-координата отрицания суммы P+Q удовлетворяет однородному полиномному тождеству, связанной с исходными выражениями addX/negAddY и коэффициентами кривой a1,..., a6.
LaTeX
$$$W'.negAddY(P,Q) \cdot (P_z Q_z)^2 = \text{(polynomial in }P,Q,a_i) \; + \; P_y Q_z (P_x Q_z - Q_x P_z)^3$$$
Lean4
/-- The `Y`-coordinate of a representative of `-(P + Q)` for two distinct projective 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 :=
-3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * P z +
W'.a₁ * P x * Q y ^ 2 * P z -
W'.a₁ * Q x * P y ^ 2 * Q z -
W'.a₂ * P x ^ 2 * Q y * Q z +
W'.a₂ * Q x ^ 2 * P y * P z +
2 * W'.a₂ * P x * Q x * P y * Q z -
2 * W'.a₂ * P x * Q x * Q y * P z -
W'.a₃ * P y ^ 2 * Q z ^ 2 +
W'.a₃ * Q y ^ 2 * P z ^ 2 +
W'.a₄ * P x * P y * Q z ^ 2 -
2 * W'.a₄ * P x * Q y * P z * Q z +
2 * W'.a₄ * Q x * P y * P z * Q z -
W'.a₄ * Q x * Q y * P z ^ 2 +
3 * W'.a₆ * P y * P z * Q z ^ 2 -
3 * W'.a₆ * Q y * P z ^ 2 * Q z
