English
When hx holds and P,Q have nonzero z, the three coordinates of P+Q are obtained by multiplying addZ(P,Q) by a 3-vector whose first two components are affine additions and the last is 1, explicitly: addXYZ P Q = addZ P Q · [toAffine.addX(...), toAffine.addY(...), 1].
Русский
При выполнении условия hx и когда z-координаты ненулевые, координаты P+Q получаются как произведение addZ(P,Q) на вектор из афинных координат: первая и вторая компоненты — афинные addX/addY, третья — 1.
LaTeX
$$$$ \\operatorname{addXYZ}(P,Q) = \\operatorname{addZ}(P,Q) \\cdot \\begin{bmatrix} \\operatorname{toAffine.addX}( \\tfrac{P_x}{P_z^2}, \\tfrac{Q_x}{Q_z^2}, \\cdots ) \\\\ \\operatorname{toAffine.addY}( \\tfrac{P_x}{P_z^2}, \\tfrac{Q_x}{Q_z^2}, \\cdots ) \\\\ 1 \\end{bmatrix} $$$$
Lean4
theorem addY_of_Z_ne_zero [DecidableEq F] {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
(hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) :
W.addY P Q / addZ P Q ^ 3 =
W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
(W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)) :=
by
erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]
