pointAdd
plain-language theorem explainer
The point addition operation on a short Weierstrass elliptic curve over a prime field is defined by case analysis on the input points. Researchers auditing discrete logarithm problems on elliptic curves would reference this as the standard chord-tangent law before applying any further invariants. The definition handles the point at infinity as the identity, returns infinity for vertical sums, and otherwise computes the third intersection point via the appropriate slope.
Claim. Let $E$ be the curve $y^2 = x^3 + a x + b$ over the field $Z/pZ$. The sum of points $P$ and $Q$ on $E$ is defined by cases: return the other point if either is the point at infinity; return the point at infinity if $P = (x_1, y_1)$ and $Q = (x_2, y_2)$ satisfy $x_1 = x_2$ and $y_1 + y_2 = 0$; otherwise compute the third point from the chord slope $(y_2 - y_1)(x_2 - x_1)^{-1}$ or the tangent slope $(3x_1^2 + a)(2y_1)^{-1}$ via the formulas $x_3 = m^2 - x_1 - x_2$, $y_3 = m(x_1 - x_3) - y_1$.
background
The module establishes an explicit surface for auditing elliptic curve discrete logarithm claims. A ShortWeierstrassCurve consists of coefficients a and b such that the equation $y^2 = x^3 + a x + b$ holds over the field ZMod p, with the discriminant condition ensuring nonsingularity. An ECPoint is either the point at infinity or an affine pair (x, y) satisfying the curve equation.
proof idea
The definition proceeds by pattern matching on the two ECPoint arguments. It returns the second point when the first is infinity, and symmetrically when the second is infinity. For two affine points it checks whether the x-coordinates coincide; if they do and the y-coordinates sum to zero it returns infinity, otherwise it applies slopeAddPoint to the tangent slope; if the x-coordinates differ it applies slopeAddPoint to the chord slope.
why it matters
This definition supplies the group operation used by scalar multiplication, which is defined by repeated application of point addition. The module as a whole provides the reference specification for an ECDLP instance on a short Weierstrass curve, allowing subsequent checks of any Recognition Science invariants on the discrete logarithm problem. It fills the role of making the standard elliptic curve arithmetic explicit before any further analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.