The chord computes the group law, and the third intersection point lies on the chord

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

Working over a field (FieldChord), the chord/tangent construction on (t, w(t)) computes the addition of points; then, over a general coefficient ring, the third intersection point of the line through two points lies on the chord (the OnLine machinery, via the Pair and SingleIota parameter specializations). This is the geometric input to the associativity of the formal group law, assembled in EllipticCurves.WeierstrassFormalGroup.GroupLaw.

The chord construction computes the group law, at the level of field identities

theorem WeierstrassCurve.chord_point_nonsingular {F : Type u_2} [Field F] (WF : WeierstrassCurve F) {q w : F} (hw : w = q ^ 3 + WF.a₁ * q * w + WF.a₂ * q ^ 2 * w + WF.a₃ * w ^ 2 + WF.a₄ * q * w ^ 2 + WF.a₆ * w ^ 3) (hw0 : w ≠ 0) (hΔ : WF.Δ ≠ 0) : WF.toAffine.Nonsingular (q / w) (-1 / w)

The parametrized point (q/w, -1/w) is nonsingular whenever (q, w) satisfies the Weierstrass equation in the (t, w)-chart and the discriminant does not vanish.

theorem WeierstrassCurve.chord_point_add {F : Type u_2} [Field F] (WF : WeierstrassCurve F) [DecidableEq F] {q₁ q₂ w₁ w₂ Λ N T₃ wT : F} (hw₁ : w₁ = q₁ ^ 3 + WF.a₁ * q₁ * w₁ + WF.a₂ * q₁ ^ 2 * w₁ + WF.a₃ * w₁ ^ 2 + WF.a₄ * q₁ * w₁ ^ 2 + WF.a₆ * w₁ ^ 3) (hw₂ : w₂ = q₂ ^ 3 + WF.a₁ * q₂ * w₂ + WF.a₂ * q₂ ^ 2 * w₂ + WF.a₃ * w₂ ^ 2 + WF.a₄ * q₂ * w₂ ^ 2 + WF.a₆ * w₂ ^ 3) (hslope : Λ * (q₂ - q₁) = w₂ - w₁) (hN : N = w₁ - Λ * q₁) (hT₃ : (1 + WF.a₂ * Λ + WF.a₄ * Λ ^ 2 + WF.a₆ * Λ ^ 3) * (T₃ + q₁ + q₂) = -(WF.a₁ * Λ + WF.a₂ * N + WF.a₃ * Λ ^ 2 + 2 * WF.a₄ * Λ * N + 3 * WF.a₆ * Λ ^ 2 * N)) (hwT : wT = Λ * T₃ + N) (hA : 1 + WF.a₂ * Λ + WF.a₄ * Λ ^ 2 + WF.a₆ * Λ ^ 3 ≠ 0) (hw₁0 : w₁ ≠ 0) (hw₂0 : w₂ ≠ 0) (hwT0 : wT ≠ 0) (hx : q₁ * w₂ - q₂ * w₁ ≠ 0) (h₁ : WF.toAffine.Nonsingular (q₁ / w₁) (-1 / w₁)) (h₂ : WF.toAffine.Nonsingular (q₂ / w₂) (-1 / w₂)) : ∃ (h₃ : WF.toAffine.Nonsingular (T₃ / wT) ((1 - WF.a₁ * T₃ - WF.a₃ * wT) / wT)), Affine.Point.some (q₁ / w₁) (-1 / w₁) h₁ + Affine.Point.some (q₂ / w₂) (-1 / w₂) h₂ = Affine.Point.some (T₃ / wT) ((1 - WF.a₁ * T₃ - WF.a₃ * wT) / wT) h₃

The chord construction computes the group law, at the level of nonsingular points.

The third intersection point lies on the chord

w(t₃(t₁, t₂)) = λ(t₁, t₂)·t₃(t₁, t₂) + ν(t₁, t₂), proved via a multivariate version of the fixed-point uniqueness engine (filtration by total degree) and the Vieta argument: the cubic obtained by substituting the chord into the Weierstrass equation has roots t₁, t₂, and its third root is t₃ by construction, so the line value at t₃ solves the Weierstrass equation there; so does w ∘ t₃, and solutions are unique.

Specialization of the chord data along a pair of parameter series (q₁, q₂) in a multivariate power series ring: the substitution plumbing feeding the identification of the addition series with the group law over the fraction field.