pointAdd
plain-language theorem explainer
pointAdd defines the chord-tangent addition law on points of a short Weierstrass curve over ZMod p, returning infinity on opposites and delegating to slopeAddPoint otherwise. Cryptographers setting up ECDLP instances for invariant testing would cite this as the reference group operation. The definition proceeds by exhaustive case split on the pair of ECPoint constructors.
Claim. On the curve $E: y^2 = x^3 + a x + b$ over $ZMod p$, the map sending a pair of points $P, Q$ to their sum $P+Q$, where the sum is the third intersection point of the line through $P$ and $Q$ (tangent when $P=Q$) with the curve and the point at infinity serves as the identity.
background
ShortWeierstrassCurve p is the structure holding the coefficients a and b for the Weierstrass equation. ECPoint p is the inductive type consisting of the point at infinity together with affine points (x, y) in ZMod p. The module constructs an explicit finite surface for auditing elliptic-curve discrete-logarithm claims, supplying the carrier, curve equation, points, and chord-tangent operation before any Recognition Science invariant is applied. Upstream chordSlope computes the secant slope (y2 - y1)(x2 - x1)^{-1}, tangentSlope applies the derivative formula involving the coefficient a, and slopeAddPoint recovers the third point via the standard slope formulas.
proof idea
Definition by pattern matching on the two ECPoint arguments. Returns the second argument when the first is infinity, the first when the second is infinity, infinity when the x-coordinates match and the y-coordinates sum to zero, otherwise selects tangentSlope or chordSlope and passes the result to slopeAddPoint.
why it matters
Supplies the group law consumed by scalarMul, which in turn populates the ECDLPInstance predicate inside the watch harness. The declaration completes the mathematical setup described in the module header for making ordinary ECDLP statements precise prior to testing any RS candidate invariant. No open question is closed here; the definition remains the reference specification rather than an optimized implementation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.