pointAdd
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not provide an efficient implementation of scalar multiplication.
- Does not verify the associative law or other group axioms for the operation.
- Does not handle curves over extension fields or rings other than prime fields.
- Does not incorporate any specific Recognition Science cost or defect measures.
formal statement (Lean)
66def pointAdd {p : ℕ} (E : ShortWeierstrassCurve p) : ECPoint p → ECPoint p → ECPoint p
67 | ECPoint.infinity, Q => Q
68 | P, ECPoint.infinity => P
69 | ECPoint.affine x₁ y₁, ECPoint.affine x₂ y₂ =>
70 if _hx : x₁ = x₂ then
71 if _hy : y₁ + y₂ = 0 then
72 ECPoint.infinity
73 else
74 slopeAddPoint (tangentSlope E x₁ y₁) x₁ y₁ x₁
75 else
76 slopeAddPoint (chordSlope x₁ y₁ x₂ y₂) x₁ y₁ x₂
77
78/-- Scalar multiplication by repeated addition. This is the reference
79specification, not an efficient implementation. -/