English
If P and Q satisfy Z ≠ 0 conditions and certain nondegeneracy inequalities fail to hold (i.e., the pair hx, hy' is not the obstruction), then the sum P + Q is the affine point with coordinates given by the standard affine addition formula.
Русский
Если P, Q удовлетворяют условиям Z ≠ 0 и не выполняются деградирующие соотношения, то сумма P + Q имеет афинные координаты, заданные обычной формулой сложения.
LaTeX
$$$ [P], [Q] \text{ with } P_z \neq 0, Q_z \neq 0, \neg( P_x Q_z = Q_x P_z \land P_y Q_z = W.negY(Q) P_z) \\Rightarrow W.addMap (\langle P \rangle) (\langle Q \rangle) = \langle [ W.toAffine.addX (P_x / P_z) (Q_x / Q_z) (W.toAffine.slope (P_x / P_z) (Q_x / Q_z) (P_y / P_z) (Q_y / Q_z)), \\ 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)), 1] \rangle $$$
Lean4
theorem nonsingularLift_addMap {P Q : PointClass F} (hP : W.NonsingularLift P) (hQ : W.NonsingularLift Q) :
W.NonsingularLift <| W.addMap P Q := by
rcases P; rcases Q
exact nonsingular_add hP hQ
