slopeAddPoint
plain-language theorem explainer
slopeAddPoint computes the affine coordinates of the third intersection point on a Weierstrass elliptic curve over Z/pZ given chord slope m and the two x-coordinates. Cryptographers building or auditing ECDLP instances over finite fields would cite it when implementing the group law. The body is a direct algebraic substitution of the standard slope formulas into the affine point constructor.
Claim. Let $p$ be a natural number and let $m,x_1,y_1,x_2$ lie in the prime field $Z/pZ$. Set $x_3 = m^2 - x_1 - x_2$ and $y_3 = m(x_1 - x_3) - y_1$. The result is the affine point with these coordinates.
background
The module supplies a minimal explicit surface for auditing elliptic-curve discrete-logarithm claims over prime fields before any Recognition Science invariant is tested. It introduces the inductive type ECPoint whose constructors are the point at infinity and an affine pair of coordinates drawn from ZMod p. The local theoretical setting is the standard chord-tangent group law on a short Weierstrass curve, with side conditions left to benchmark code.
proof idea
The definition performs direct substitution: it calculates the third x-coordinate from the slope formula, derives the corresponding y-coordinate, and applies the affine constructor of ECPoint. No lemmas are invoked; the body is a pure algebraic abbreviation.
why it matters
The definition is called by pointAdd, which realizes the complete chord-tangent addition formula. It therefore supplies the concrete arithmetic needed to make the ECDLP group operation precise inside the cryptography audit surface. The surrounding module exists to render the ordinary mathematical problem explicit so that any later Recognition Science candidate (J-cost, phi-ladder, etc.) can be checked against standard instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.