English
If P, Q lie on the Weierstrass curve with Y-relations, then the product negDblY P and P z^2 equals a specific polynomial expression in eval P W'.polynomialX, P_x, P_y, and P_z, simplifying to a standard formula.
Русский
Если P, Q лежат на кривой Вейерштрасса и удовлетворяют Y-отношениям, то NegDblY P · P z^2 выражается через некоторый многочлен в eval P W'.polynomialX и координатах P.
LaTeX
$$$ {P Q: Fin 3 → F} (hP: W'.Equation P) (hQ: W'.Equation Q) \Rightarrow W'.negDblY P \cdot P z^2 = -\mathrm{eval} P W'.polynomialX^3$$$
Lean4
theorem negDblY_eq' {P : Fin 3 → R} (hP : W'.Equation P) :
W'.negDblY P * P z ^ 2 =
-eval P W'.polynomialX *
(eval P W'.polynomialX ^ 2 - W'.a₁ * eval P W'.polynomialX * P z * (P y - W'.negY P) -
W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
2 * P x * P z * (P y - W'.negY P) ^ 2 -
P x * P z * (P y - W'.negY P) ^ 2) +
P y * P z ^ 2 * (P y - W'.negY P) ^ 3 :=
by
linear_combination (norm := (rw [negDblY, eval_polynomialX, negY]; ring1))
-9 * (P y ^ 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * P x ^ 3 - 3 * W'.a₂ * P x ^ 2 * P z) *
(equation_iff _).mp hP
