English
Assume P,Q satisfy W'.Equation P, W'.Equation Q and P_z ≠ 0, Q_z ≠ 0, with hx ≠ relation. Then the projective Y-coordinate scaled by addZ^3 matches the affine Y-coordinate computed from normalized coordinates with the affine slope: W.addY P Q / addZ^3 = W.toAffine.addY(...).
Русский
Пусть P,Q удовлетворяют условиям наEquation и z-координаты ненулевые; тогда псевдоскалированная Y-координата проекта равна афинной Y-координате с использованием нормализованных координат и аппроксимации наклона: W.addY P Q / addZ(P,Q)^3 = W.toAffine.addY(...).
LaTeX
$$$$ \\frac{W.addY(P,Q)}{(addZ(P,Q))^3} = W.toAffine.addY\\Big( \\frac{P_x}{P_z^2}, \\frac{Q_x}{Q_z^2}, \\frac{P_y}{P_z^3}, \\text{Slope}(\\frac{P_x}{P_z^2},\\frac{Q_x}{Q_z^2},\\frac{P_y}{P_z^3},\\frac{Q_y}{Q_z^3}) \\Big) $$$$
Lean4
theorem addY_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
W'.addY P Q * (P z * Q z) ^ 3 = (-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 := by
linear_combination (norm := (rw [addY, negY_eq, addZ_of_X_eq hx]; ring1)) -negAddY_of_X_eq' hP hQ hx
