English
Under a primed Y-equality hy' with Z ≠ 0, addMap(P,Q) equals the doubled Z-map times a specific affine coordinate vector involving addX/addY.
Русский
При условии Y-равенства hy' с Z ≠ 0 сумма P+Q равна удвоенному Z-образу, умноженному на конкретный аффинный вектор с addX/addY.
LaTeX
$$W'.addMap ⟦P⟧ ⟦Q⟧ = W.dblZ P · ⟦[W.toAffine.addX(…), W.toAffine.addY(…), 1]⟧$$
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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)) :
W.addMap ⟦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
by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2
·
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 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 hx]
