English
If P and Q are points on W with Y-compatibility (i.e., certain relations among coordinates hold), then their sum is the doubling of P scaled by the vector [1,1,0] along the Jacobian's affine structure: W.add P Q = W.dblU P · [1,1,0].
Русский
Если точки P и Q удовлетворяют условию согласованности Y-координат, то сумма P+Q равна удвоению P, домноженному на вектор [1,1,0] в аффинной структуре Якобиана: W.add P Q = W.dblU P · [1,1,0].
LaTeX
$$$W.add\,P\,Q = W.dblU\,P \cdot \begin{bmatrix}1\\1\\0\end{bmatrix}$$$
Lean4
theorem add_of_Y_eq {P Q : Fin 3 → F} (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 = Q y * P z ^ 3) (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) :
W.add P Q = W.dblU P • ![1, 1, 0] := by
rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hQz hx hy hy']
