English
In the Y-equality variant with Y' (hy'), the sum equals the doubled point along Z, i.e. W.add P Q = W.dblZ P · ⟦W.toAffine.addX(...), W.toAffine.addY(...), 1⟧, where the X and Y coordinates are determined by affine formulas between P and Q.
Русский
В случае Y' (hy') сумма P+Q равна удвоению по Z, то есть W.add P Q = W.dblZ P · ⟦[аддX, аддY, 1]⟧, где координаты X и Y задаются через аффинные формулы зависимости между P и Q.
LaTeX
$$$W.add\,P\,Q = W.dblZ\,P \cdot \Big\lbrack W.toAffine.addX\big( \frac{P_0}{P_2^2}, \frac{Q_0}{Q_2^2} \Big),\; W.toAffine.addY\big( \frac{P_0}{P_2^2}, \frac{Q_0}{Q_2^2} \Big), 1 \Big\rbrack$$$
Lean4
theorem add_of_Y_ne' [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) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
W.add P Q =
W.dblZ P •
![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
(W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 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)),
1] :=
by
rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hx hy,
dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]
