English
Let P and Q be nonsingular points with nonzero z-coordinates. If the condition of not being aligned (no hx, hy' pair) holds, then the sum P + Q equals the projective point determined by the slope and intercept given by the standard affine addition formulas.
Русский
Пусть P и Q — ненонсиглярные точки с ненулевыми z-координатами. Если выполняется условие непараллельности (нет пары hx, hy'), то сумма P + Q равна проективной точке, заданной наклоном и перехватом по стандартным формулам афинного сложения.
LaTeX
$$$ (W.Equation P) \land (W.Equation Q) \land (P_z \neq 0) \land (Q_z \neq 0) \Rightarrow \\ W.addMap (P) (Q) = \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 addMap_of_Z_ne_zero [DecidableEq F] {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
(hQz : Q z ≠ 0) (hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)) :
W.addMap ⟦P⟧ ⟦Q⟧ =
⟦![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]⟧ :=
by
by_cases hx : P x * Q z = Q x * P z
·
rw [addMap_eq, add_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx,
smul_eq _ <| isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx <| not_and.mp hxy hx]
· rw [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hP hQ hx]
