English
If two points are on the curve with x-coordinates x1 ≠ x2, then the polynomial for their sum along the line of slope slope(x1,x2, y1,y2) factors as a cubic with roots at x1, x2, and the x-coordinate of P1+P2.
Русский
Если две точки кривой имеют различные x-координаты x1 ≠ x2, то полином сложения вдоль прямой с углом наклона slope(x1,x2,y1,y2) раскладывается как произведение кубика с корнями в x1, x2 и x3, где x3 — координата x суммы P1+P2.
LaTeX
$$$ W'.addPolynomial x_1 y_1 (W.slope x_1 x_2 y_1 y_2) = -\left( X - C x_1\right)\left( X - C x_2\right)\left( X - C\bigl(W.addX x_1 x_2 (W.slope x_1 x_2 y_1 y_2)\bigr)\right)$$$
Lean4
theorem 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₂)) :
W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
by
rw [addPolynomial_eq, neg_inj, Cubic.prod_X_sub_C_eq, Cubic.toPoly_injective]
by_cases hx : x₁ = x₂
· have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
rw [equation_iff] at h₁ h₂
rw [slope_of_Y_ne rfl hy]
rw [negY, ← sub_ne_zero] at hy
replace hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0 := by convert hy using 1; ring
ext
· rfl
· simp only [addX]
ring1
· simp [field]
ring1
· linear_combination (norm := (simp [field]; ring1)) -h₁
· rw [equation_iff] at h₁ h₂
rw [slope_of_X_ne hx]
rw [← sub_eq_zero] at hx
ext
· rfl
· simp only [addX]
ring1
· apply mul_right_injective₀ hx
linear_combination (norm := (simp [field]; ring1)) h₂ - h₁
· apply mul_right_injective₀ hx
linear_combination (norm := (simp [field]; ring1)) x₂ * h₁ - x₁ * h₂
