English
Let W be a Weierstrass curve in projective form over a field F, and let P,Q be two points on W with nonzero z-coordinates. If P and Q satisfy the standard cross-relations, then the slope-based affine expression for the Y-coordinate of 2P equals the ratio of Y and Z components, i.e. dblY P / dblZ P = addY( P_x/P_z, Q_x/Q_z, P_y/P_z )( slope( ... ) ).
Русский
Пусть W — проективная кривая Вейерштрасса над полем F, и пусть P,Q — точки на W с ненулевыми z-координатами. При соблюдении стандартных накрест-равенств между координатами точек, отношение dblY P к dblZ P равно коэффициенту в affine-представлении, задаваемому через addY и slope.
LaTeX
$$$\forall F\ (P,Q:\ Fin(3) \to F),\ W: WeierstrassCurve.Projective\ F,\ hP: W.Equation(P),\ hQ: W.Equation(Q),\ hPz: P_z \neq 0,\ hQz: Q_z \neq 0,\ hx: P_x Q_z = Q_x P_z,\ hy: P_y Q_z \neq W.negY(Q) P_z:\n\frac{W.dblY(P)}{W.dblZ(P)} = W.toAffine.addY( P_x/P_z, Q_x/Q_z, P_y/P_z)\big( W.toAffine.slope( P_x/P_z, Q_x/Q_z, P_y/P_z, Q_y/Q_z) \big)$$$
Lean4
theorem dblY_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) (hy : P y * Q z ≠ W.negY Q * P z) :
W.dblY P / W.dblZ P =
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 [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz hx hy, dblX_of_Z_ne_zero hP hQ hPz hQz hx hy,
negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]
