English
Let P,Q be points with W.Equation P, W.Equation Q in a Weierstrass Jacobian over a field F, with P_z ≠ 0 and Q_z ≠ 0. If hx: P_x Q_z^2 ≠ Q_x P_z^2, then the affine Y-coordinate relation holds: W.negAddY P Q / addZ P Q^3 = W.toAffine.negAddY (P_x / P_z^2) (Q_x / Q_z^2) (P_y / P_z^3) (W.toAffine.slope(...)).
Русский
Пусть P,Q—точки на кривой Вейерштрасса в Якобиане над полем F; P_z ≠ 0, Q_z ≠ 0 и hx: P_x Q_z^2 ≠ Q_x P_z^2. Тогда отношение афинной Y-компоненты верно: W.negAddY P Q / addZ P Q^3 = W.toAffine.negAddY( P_x / P_z^2, Q_x / Q_z^2, P_y / P_z^3, W.toAffine.slope(...)).
LaTeX
$$$$ \\frac{W.negAddY(P,Q)}{(addZ(P,Q))^3} = W.toAffine.negAddY\\left( \\frac{P_x}{P_z^2}, \\frac{Q_x}{Q_z^2}, \\frac{P_y}{P_z^3}, W.toAffine.slope\\left( \\frac{P_x}{P_z^2}, \\frac{Q_x}{Q_z^2}, \\frac{P_y}{P_z^3}, \\frac{Q_y}{Q_z^3} \\right) \\right) $$$$
Lean4
theorem negAddY_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.negAddY P Q / addZ P Q ^ 3 =
W.toAffine.negAddY (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
rw [negAddY_eq hPz hQz, addX_eq' hP hQ, toAffine_slope_of_ne hPz hQz hx,
toAffine_negAddY_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]
