English
For P,Q on the curve with nonzero Z components and hx, hy, the ratio dblX P / dblZ P^2 equals the affine X-entry of the sum on the Weierstrass curve.
Русский
Для P,Q на кривой с ненулевыми Z-компонентами и условиях hx, hy, отношение dblX P / dblZ P^2 равно аффинной X-координате суммы на кривой Вейерштрасса.
LaTeX
$$For hP,hQ, hx, hy: $\frac{W.dblX P}{W.dblZ P^2} = 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))$$$
Lean4
theorem dblX_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) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
W.dblX P / W.dblZ P ^ 2 =
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)) :=
by
rw [dblX, toAffine_slope_of_eq hP hQ hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
toAffine_addX_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]
