English
The same slope-based addition polynomial has its coefficients encoded as a negative cubic polynomial with Weierstrass coefficients a1,...,a6.
Русский
Тот же полином сложения по наклону имеет коэффициенты, закодированные как минус кубического многочлена с коэффициентами Вейерштраса a1,...,a6.
LaTeX
$$W'.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = -\mathrm{Cubic.toPoly}\langle 1, -\ell^{2} - W'.a₁ \ell + W'.a₂, 2 x₁ \ell^{2} + (W'.a₁ x₁ - 2 y₁ - W'.a₃) \ell + (-W'.a₁ y₁ + W'.a₄), -x₁^{2} \ell^{2} + (2 x₁ y₁ + W'.a₃ x₁) \ell - (y₁^{2} + W'.a₃ y₁ - W'.a₆)\rangle$$
Lean4
theorem C_addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
(hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
C (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
-(C (X - C x₁) * C (X - C x₂) * C (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
by
rw [addPolynomial_slope h₁ h₂ hxy]
simp
