English
If P and Q lie on W with P_z ≠ 0 and Q_z ≠ 0 and cross-relations hold, then the affine Y-coordinate of the doubling is given by an affine expression involving the slope between scaled X-coordinates.
Русский
Если P и Q лежат на W, P_z ≠ 0, Q_z ≠ 0 и соблюдаются накрест-равенства, то аффинная Y-координата удвоения выражается через наклон и масштабы X-координат.
LaTeX
$$$\forall F\ [Field 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\dots \Rightarrow \frac{W.dblY(P)}{W.dblZ(P)} = W.toAffine.addY\left(\frac{P_x}{P_z},\frac{Q_x}{Q_z},\frac{P_y}{P_z}\right)\left( 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 addZ_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
W.addZ P Q = (P x * Q z - Q x * P z) ^ 3 / (P z * Q z) := by
rw [← addZ_eq' hP hQ, mul_div_cancel_right₀ _ <| mul_ne_zero hPz hQz]
