English
Let P,Q be on a Weierstrass projective curve with P2 ≠ 0, Q2 ≠ 0, and P x Q z ≠ Q x P z. Then the affine Y-coordinate of P+Q is given by the affine addition formula: (W.addY P Q)/(W.addZ P Q) = W.toAffine.addY( P_x/P_z, Q_x/Q_z, P_y/P_z, slope(...) ).
Русский
Пусть P,Q лежат на проективной кривой Вейерштрасса, P2 ≠ 0, Q2 ≠ 0, и P x Q z ≠ Q x P z. Тогда аффинная y-координата суммы дана афинной формулой сложения: (W.addY P Q)/(W.addZ P Q) = W.toAffine.addY(...).
LaTeX
$$$\dfrac{W.addY(P,Q)}{W.addZ(P,Q)} = W.toAffine.addY\left(\frac{P_x}{P_z},\frac{Q_x}{Q_z},\frac{P_y}{P_z},\;W.toAffine.slope\left(\frac{P_x}{P_z},\frac{Q_x}{Q_z},\frac{P_y}{P_z},\frac{Q_y}{Q_z}\right)\right)$$$
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 ≠ Q x * P z) :
W.addY P Q / W.addZ P Q =
W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
(W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)) :=
by
erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]
