Build the idea in three steps
- On a nonsingular Weierstrass curve, the third intersection R of the line through P and Q is not yet P + Q: the sum is −R. For a short equation y² = x³ + Ax + B, negate by reflecting across the x-axis. In the general equation, −(x,y) = (x, −y − a₁x − a₃). Coincident points use a tangent; inverse points sum to the identity at infinity.
- The displayed instance lets the symmetry actors of the number world touch the curve: σ • P applies σ to the coordinates of P, producing another point. It is a DistribMulAction — the identity leaves points alone, and doing σ then τ is one combined shuffle.
- The last line is the hinge for everything later: smul_add certifies σ • (P + Q) = σ • P + σ • Q, proved by map_add on the underlying map. Symmetries of the number world respect the curve’s own addition — precisely the agreement that will let a representation record the curve.
A small example
On y² = x³ − x + 1, P = (0,1) and Q = (1,1) lie on y = 1. Its third intersection is R = (−1,1), so P + Q = −R = (−1,−1). Taking the third intersection without negating it would give the wrong sum.