English
The X-coordinate of P+Q in Jacobian coordinates equals a rational expression in P,Q. Under certain non-degeneracy hypotheses, it equals the above explicit formula.
Русский
X-координата суммы P+Q в координатах Якобиана равна явному дробно-рациональному выражению через координаты P и Q при некоторых ненулевых условиях.
LaTeX
$$For W', P, Q with P,Q satisfying W'.Equation and non-degeneracy, W'.addX P Q equals the explicit expression dividing by (Pz Qz)^2.$$
Lean4
/-- The `X`-coordinate of a representative of `P + Q` for two distinct Jacobian 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 x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * Q z -
W'.a₁ * P y * Q x * P z * Q z ^ 2 +
2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
W'.a₃ * Q y * P z ^ 4 * Q z -
W'.a₃ * P y * P z * Q z ^ 4 +
W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
2 * W'.a₆ * P z ^ 4 * Q z ^ 4
