English
There is a relation expressing negDblY P in terms of the polynomial X and y-coordinates when P and Q satisfy the Weierstrass relations and the Y-relations hold with hy'.
Русский
Существует формула, связывающая negDblY P с X-полином и Y-координатами при выполнении условий на W'.Equation и Y-отношениях hy'.
LaTeX
$$$ {P Q: Fin 3 → F} (hP: W'.Equation P) (hQ: W'.Equation Q) (hPz: P z ≠ 0) (hQz: Q z ≠ 0) (hx: P x Q z = Q x P z) (hy: P y Q z ≠ W'.negY Q P z) (hy': P y Q z = W'.negY Q P z) : W'.negDblY P \cdot P z^2 = \cdots $$$
Lean4
/-- The `Y`-coordinate of a representative of `-(2 • P)` for a projective point representative `P`
on a Weierstrass curve. -/
noncomputable def negDblY (P : Fin 3 → R) : R :=
-P y ^ 4 - 3 * W'.a₁ * P x * P y ^ 3 - 9 * W'.a₃ * P x ^ 3 * P y + 3 * W'.a₃ * P y ^ 3 * P z -
3 *
W'.a₄ *
P
x *
P
y ^
2 *
P z -
27 *
W'.a₆ *
P x ^
3 *
P z +
9 * W'.a₆ *
P y ^
2 *
P z ^ 2 -
3 *
W'.a₁ ^
2 *
P x ^ 2 *
P y ^ 2 +
4 * W'.a₁ *
W'.a₂ *
P y ^ 3 *
P z -
3 * W'.a₁ *
W'.a₂ *
P x ^ 3 *
P y -
9 * W'.a₁ * W'.a₃ *
P x ^ 4 +
6 * W'.a₁ * W'.a₃ *
P x *
P y ^ 2 *
P z +
18 * W'.a₁ * W'.a₆ *
P x *
P y *
P z ^ 2 +
9 * W'.a₂ ^ 2 * P x ^ 4 -
8 * W'.a₂ ^ 2 * P x *
P y ^ 2 *
P z -
9 * W'.a₂ * W'.a₃ * P x ^ 2 *
P y *
P z +
9 * W'.a₂ * W'.a₄ * P x ^ 3 *
P z -
4 * W'.a₂ * W'.a₄ * P y ^ 2 *
P z ^ 2 -
27 * W'.a₂ * W'.a₆ * P x ^ 2 *
P z ^ 2 -
9 * W'.a₃ ^ 2 * P x ^ 3 * P z +
6 * W'.a₃ ^ 2 * P y ^ 2 * P z ^ 2 -
12 * W'.a₃ * W'.a₄ * P x * P y * P z ^ 2 +
9 * W'.a₄ ^ 2 * P x ^ 2 * P z ^ 2 -
2 * W'.a₁ ^ 3 * P x ^ 3 * P y +
W'.a₁ ^ 3 * P y ^ 3 * P z +
3 * W'.a₁ ^ 2 * W'.a₂ * P x ^ 4 +
2 * W'.a₁ ^ 2 * W'.a₂ * P x * P y ^ 2 * P z +
3 * W'.a₁ ^ 2 * W'.a₃ * P x ^ 2 * P y * P z +
3 * W'.a₁ ^ 2 * W'.a₄ * P x ^ 3 * P z -
W'.a₁ ^ 2 * W'.a₄ * P y ^ 2 * P z ^ 2 -
12 * W'.a₁ * W'.a₂ ^ 2 * P x ^ 2 * P y * P z -
6 * W'.a₁ * W'.a₂ * W'.a₃ * P x ^ 3 * P z +
4 * W'.a₁ * W'.a₂ * W'.a₃ * P y ^ 2 * P z ^ 2 -
8 * W'.a₁ * W'.a₂ * W'.a₄ * P x * P y * P z ^ 2 +
6 * W'.a₁ * W'.a₃ ^ 2 * P x * P y * P z ^ 2 -
W'.a₁ * W'.a₄ ^ 2 * P y * P z ^ 3 +
8 * W'.a₂ ^ 3 * P x ^ 3 * P z -
8 * W'.a₂ ^ 2 * W'.a₃ * P x * P y * P z ^ 2 +
12 * W'.a₂ ^ 2 * W'.a₄ * P x ^ 2 * P z ^ 2 -
9 * W'.a₂ * W'.a₃ ^ 2 * P x ^ 2 * P z ^ 2 -
4 * W'.a₂ * W'.a₃ * W'.a₄ * P y * P z ^ 3 +
6 * W'.a₂ * W'.a₄ ^ 2 * P x * P z ^ 3 +
W'.a₃ ^ 3 * P y * P z ^ 3 -
3 * W'.a₃ ^ 2 * W'.a₄ * P x * P z ^ 3 +
W'.a₄ ^ 3 * P z ^ 4 +
W'.a₁ ^ 4 * P x * P y ^ 2 * P z -
3 * W'.a₁ ^ 3 * W'.a₂ * P x ^ 2 * P y * P z +
W'.a₁ ^ 3 * W'.a₃ * P y ^ 2 * P z ^ 2 -
2 * W'.a₁ ^ 3 * W'.a₄ * P x * P y * P z ^ 2 +
2 * W'.a₁ ^ 2 * W'.a₂ ^ 2 * P x ^ 3 * P z -
2 * W'.a₁ ^ 2 * W'.a₂ * W'.a₃ * P x * P y * P z ^ 2 +
3 * W'.a₁ ^ 2 * W'.a₂ * W'.a₄ * P x ^ 2 * P z ^ 2 -
2 * W'.a₁ ^ 2 * W'.a₃ * W'.a₄ * P y * P z ^ 3 +
W'.a₁ ^ 2 * W'.a₄ ^ 2 * P x * P z ^ 3 +
W'.a₁ * W'.a₂ * W'.a₃ ^ 2 * P y * P z ^ 3 +
2 * W'.a₁ * W'.a₂ * W'.a₃ * W'.a₄ * P x * P z ^ 3 +
W'.a₁ * W'.a₃ * W'.a₄ ^ 2 * P z ^ 4 -
2 * W'.a₂ ^ 2 * W'.a₃ ^ 2 * P x * P z ^ 3 -
W'.a₂ * W'.a₃ ^ 2 * W'.a₄ * P z ^ 4
