English
There is a formula for the X-coordinate of 2P, given P satisfies the Weierstrass Equation W'.Equation P. The product W'.dblX P · P z equals a certain polynomial in eval P W'.polynomialX, the x- and y-coordinates and P z, multiplied by (P y − W'.negY P).
Русский
Существует формула для X-координаты точки 2P, если P удовлетворяет уравнению W'.Equation P. Произведение W'.dblX P · P z равно многочлену, зависящему от eval P W'.polynomialX, координат x,y и P_z, умноженному на (P_y − W'.negY P).
LaTeX
$$$ {P: \mathrm{Fin}(3)→R} \; (hP: W'.Equation P) : \; W'.dblX P \cdot P z = \big( \mathrm{eval} P W'.polynomialX^2 - W'.a_1 \cdot \mathrm{eval} P W'.polynomialX \cdot P z \cdot (P_y - W'.negY P) - W'.a_2 \cdot P_z^2 \cdot (P_y - W'.negY P)^2 - 2 P_x P_z (P_y - W'.negY P)^2 \big) \cdot (P_y - W'.negY P) $$$
Lean4
/-- The `X`-coordinate of a representative of `2 • P` for a projective point representative `P` on a
Weierstrass curve. -/
noncomputable def dblX (P : Fin 3 → R) : R :=
2 * P x * P y ^ 3 + 3 * W'.a₁ * P x ^ 2 * P y ^ 2 + 6 * W'.a₂ * P x ^ 3 * P y - 8 * W'.a₂ * P y ^ 3 * P z +
9 * W'.a₃ * P x ^ 4 -
6 * W'.a₃ * P x * P y ^ 2 *
P z -
6 * W'.a₄ * P x ^ 2 * P y * P z -
18 * W'.a₆ * P x * P y * P z ^ 2 +
3 * W'.a₁ ^ 2 * P x ^ 3 * P y -
2 * W'.a₁ ^ 2 * P y ^ 3 * P z +
3 * W'.a₁ * W'.a₂ * P x ^ 4 -
12 * W'.a₁ * W'.a₂ * P x * P y ^ 2 * P z -
9 * W'.a₁ * W'.a₃ * P x ^ 2 * P y * P z -
3 * W'.a₁ * W'.a₄ * P x ^ 3 * P z -
9 * W'.a₁ * W'.a₆ * P x ^ 2 * P z ^ 2 +
8 * W'.a₂ ^ 2 * P x ^ 2 * P y * P z +
12 * W'.a₂ * W'.a₃ * P x ^ 3 * P z -
12 * W'.a₂ * W'.a₃ * P y ^ 2 * P z ^ 2 +
8 * W'.a₂ * W'.a₄ * P x * P y * P z ^ 2 -
12 * W'.a₃ ^ 2 * P x * P y * P z ^ 2 +
6 * W'.a₃ * W'.a₄ * P x ^ 2 * P z ^ 2 +
2 * W'.a₄ ^ 2 * P y * P z ^ 3 +
W'.a₁ ^ 3 * P x ^ 4 -
3 * W'.a₁ ^ 3 * P x * P y ^ 2 * P z -
2 * W'.a₁ ^ 2 * W'.a₂ * P x ^ 2 * P y * P z -
3 * W'.a₁ ^ 2 * W'.a₃ * P y ^ 2 * P z ^ 2 +
2 * W'.a₁ ^ 2 * W'.a₄ * P x * P y * P z ^ 2 +
4 * W'.a₁ * W'.a₂ ^ 2 * P x ^ 3 * P z -
8 * W'.a₁ * W'.a₂ * W'.a₃ * P x * P y * P z ^ 2 +
4 * W'.a₁ * W'.a₂ * W'.a₄ * P x ^ 2 * P z ^ 2 -
3 * W'.a₁ * W'.a₃ ^ 2 * P x ^ 2 * P z ^ 2 +
2 * W'.a₁ * W'.a₃ * W'.a₄ * P y * P z ^ 3 +
W'.a₁ * W'.a₄ ^ 2 * P x * P z ^ 3 +
4 * W'.a₂ ^ 2 * W'.a₃ * P x ^ 2 * P z ^ 2 -
6 * W'.a₂ * W'.a₃ ^ 2 * P y * P z ^ 3 +
4 * W'.a₂ * W'.a₃ * W'.a₄ * P x * P z ^ 3 -
2 * W'.a₃ ^ 3 * P x * P z ^ 3 +
W'.a₃ * W'.a₄ ^ 2 * P z ^ 4 -
W'.a₁ ^ 4 * P x ^ 2 * P y * P z +
W'.a₁ ^ 3 * W'.a₂ * P x ^ 3 * P z -
2 * W'.a₁ ^ 3 * W'.a₃ * P x * P y * P z ^ 2 +
W'.a₁ ^ 3 * W'.a₄ * P x ^ 2 * P z ^ 2 +
W'.a₁ ^ 2 * W'.a₂ * W'.a₃ * P x ^ 2 * P z ^ 2 -
W'.a₁ ^ 2 * W'.a₃ ^ 2 * P y * P z ^ 3 +
2 * W'.a₁ ^ 2 * W'.a₃ * W'.a₄ * P x * P z ^ 3 -
W'.a₁ * W'.a₂ * W'.a₃ ^ 2 * P x * P z ^ 3 -
W'.a₂ * W'.a₃ ^ 3 * P z ^ 4 +
W'.a₁ * W'.a₃ ^ 2 * W'.a₄ * P z ^ 4
