English
Scaling inputs scales the Z-coordinate portion of addZ by the square of the scale factor: addZ(u·P, v·Q) = (u v)^2 · addZ(P,Q).
Русский
Умножение входов на масштабы масштабирует Z-координату: addZ(u·P, v·Q) = (u v)^2 · addZ(P,Q).
LaTeX
$$$W'.addZ(u\cdot P, v\cdot Q) = (u v)^2 \cdot W'.addZ(P,Q)$$$
Lean4
/-- The `Z`-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 addZ (P Q : Fin 3 → R) : R :=
-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
W'.a₁ * P x * P y * Q z ^ 2 -
W'.a₁ * Q x * Q y * P z ^ 2 -
W'.a₂ * P x ^ 2 * Q z ^ 2 +
W'.a₂ * Q x ^ 2 * P z ^ 2 +
W'.a₃ * P y * P z * Q z ^ 2 -
W'.a₃ * Q y * P z ^ 2 * Q z -
W'.a₄ * P x * P z * Q z ^ 2 +
W'.a₄ * Q x * P z ^ 2 * Q z
