English
If hx (P_x Q_z^2 ≠ Q_x P_z^2), then the sum W.add P Q equals addZ P Q scaled by the affine X and Y components given by addX/addY, i.e., W.add P Q = addZ P Q · ⟦W.toAffine.addX(...), W.toAffine.addY(...), 1⟧.
Русский
Если выполняется неравенство по X: P_x Q_z^2 ≠ Q_x P_z^2, тогда сумма W.add P Q равна addZ P Q, умноженному на вектор, задаваемый addX/addY, т.е. W.add P Q = addZ P Q · ⟦[addX(...), addY(...), 1]⟧.
LaTeX
$$$W.add\,P\,Q = addZ\,P\,Q \cdot \Big\lbrack W.toAffine.addX\big( \frac{P_0}{P_2^2}, \frac{Q_0}{Q_2^2} \,,\frac{P_1}{P_2^3} \,,\frac{Q_1}{Q_2^3} \big),\; W.toAffine.addY\big( \frac{P_0}{P_2^2}, \frac{Q_0}{Q_2^2} \,,\frac{P_1}{P_2^3} \,,\frac{Q_1}{Q_2^3} \big), 1\Big\rbrack$$$
Lean4
theorem add_of_X_ne [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) :
W.add P Q =
addZ P Q •
![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)),
W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
(W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
1] :=
by rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]
