English
Let P and Q be Jacobian points on a Weierstrass curve, represented by triples P = (P_x, P_y, P_z) and Q = (Q_x, Q_y, Q_z) in some ring R. Then the Z-coordinate of a representative of the sum P + Q is given by addZ(P,Q) = P_x Q_z^2 − Q_x P_z^2. In particular, if P and Q represent the same point, this quantity is 0.
Русский
Пусть P и Q — точки Якобиана на кривой Вейерштрасса, задаваемые тройками P = (P_x, P_y, P_z) и Q = (Q_x, Q_y, Q_z) в некотором кольце. Тогда Z-координата представителя суммы P + Q равна addZ(P,Q) = P_x Q_z^2 − Q_x P_z^2. В частности, если P и Q совпадают, то эта величина равна 0.
LaTeX
$$$\operatorname{addZ}(P,Q) = P_x \; Q_z^2 - Q_x \; P_z^2$$$
Lean4
/-- The `Z`-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 addZ (P Q : Fin 3 → R) : R :=
P x * Q z ^ 2 - Q x * P z ^ 2
