English
Let W be a Weierstrass Jacobian over fields and P a triple in F^3 representing a projective point with P z ≠ 0. Then the X-coordinate computed by evaluating the Jacobian polynomial X at P, normalized by P z^4, equals the affine X-coordinate obtained from W via the coordinates (P x / P z^2, P y / P z^3).
Русский
Пусть W — Якобиан Вейерштрасса над полем, а P — тройка элементов поля, задающая проективную точку с P z ≠ 0. Тогда X-координата, получаемая из полинома W.polynomialX в P и нормированная на P z^4, равна аффинной X-координате, полученной из W для коэффициентов (P x / P z^2, P y / P z^3).
LaTeX
$$$\\text{Let } P : \\mathrm{Fin}\\,3 \\to F, \\; P z \\neq 0.\\quad \\operatorname{eval} P\\,W.polynomialX \,/\, P z^{4} = W.toAffine.polynomialX.evalEval\\bigl( P x / P z^{2},\\; P y / P z^{3} \\bigr).$$$
Lean4
theorem eval_polynomialX_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
eval P W.polynomialX / P z ^ 4 = W.toAffine.polynomialX.evalEval (P x / P z ^ 2) (P y / P z ^ 3) := by
linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
W.a₁ * P y / P z ^ 3 * div_self hPz - 2 * W.a₂ * P x / P z ^ 2 * div_self (pow_ne_zero 2 hPz) -
W.a₄ * div_self (pow_ne_zero 4 hPz)
