English
For P, Q ∈ (Fin 3 → R) lying on a Weierstrass curve W’ over a ring R, the X-coordinate of P+Q is given by a specific homogeneous rational expression in the coordinates of P and Q, with denominator (Pz Qz)^2 and a factor (Px Qz − Qx Pz).
Русский
Для P, Q ∈ (Fin 3 → R), лежащих на кривой Вейершстраса W’, X-координата суммы P+Q определяется конкретным однородно-дробно-рациональным выражением по координатам P и Q, с знаменателем (Pz Qz)^2 и множителем (Px Qz − Qx Pz).
LaTeX
$$$W'.addX(P,Q) = \dfrac{(P_y Q_z - Q_y P_z)^2 P_z Q_z + a_1 (P_y Q_z - Q_y P_z) P_z Q_z (P_x Q_z - Q_x P_z) - a_2 P_z Q_z (P_x Q_z - Q_x P_z)^2 - P_x Q_z (P_x Q_z - Q_x P_z)^2 - Q_x P_z (P_x Q_z - Q_x P_z)^2}{(P_z Q_z)^2} (P_x Q_z - Q_x P_z),$$
Lean4
/-- The `X`-coordinate of a representative of `P + Q` for two distinct projective point
representatives `P` and `Q` on a Weierstrass curve.
If the representatives of `P` and `Q` are equal, then this returns the value `0`. -/
def addX (P Q : Fin 3 → R) : R :=
-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
W'.a₁ * P x ^ 2 * Q y * Q z +
W'.a₁ * Q x ^ 2 * P y * P z +
W'.a₂ * P x ^ 2 * Q x * Q z -
W'.a₂ * P x * Q x ^ 2 * P z -
W'.a₃ * P x * P y * Q z ^ 2 +
W'.a₃ * Q x * Q y * P z ^ 2 -
2 * W'.a₃ * P x * Q y * P z * Q z +
2 * W'.a₃ * Q x * P y * P z * Q z +
W'.a₄ * P x ^ 2 * Q z ^ 2 -
W'.a₄ * Q x ^ 2 * P z ^ 2 +
3 * W'.a₆ * P x * P z * Q z ^ 2 -
3 * W'.a₆ * Q x * P z ^ 2 * Q z
