English
Let W be a Weierstrass curve in projective form over a field F. For two projective point representatives P and Q that lie on W, satisfy the defining equations, and have nonzero z-coordinates, together with certain cross-relations among their homogeneous coordinates, the Y-coordinate of doubling P equals the corresponding U-coordinate after doubling: dblY P = dblU P.
Русский
Пусть W — кривоя Вейерштрасса в проективной форме над полем F. Пусть P и Q — представления точек на W, удовлетворяющие определяющим уравнениям, z-координаты которых ненулевые, и выполняются определённые накрест равенства их однородных координат; тогда Y-координата удвоения P совпадает с соответствующей координатой U после удвоения: dblY P = dblU P.
LaTeX
$$$\forall F\ (W\,:\ WeierstrassCurve.Projective\ F),\forall P,Q:\ Fin(3) \to F,\ W.Equation(P)\land W.Equation(Q)\land P_z \neq 0\land Q_z \neq 0\land P_x Q_z = Q_x P_z\land P_y Q_z = Q_y P_z\land P_y Q_z = W.negY(Q) P_z\Rightarrow W.dblY(P) = W.dblU(P)$$$
Lean4
theorem dblY_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
(hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) : W.dblY P = W.dblU P := by
rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
