ECPoint
plain-language theorem explainer
The declaration introduces the inductive carrier for points on a short Weierstrass elliptic curve over the prime field Z/pZ. Researchers stating concrete ECDLP instances inside the Recognition Science watch harness cite this type when they need an explicit point set before testing candidate invariants. The definition is a standard two-constructor inductive that equips infinity as group identity and affine pairs for ordinary points, with DecidableEq and Repr derived automatically.
Claim. Let $p$ be a natural number. The point set of the elliptic curve consists of the point at infinity together with all pairs $(x,y)$ where $x,y$ belong to the prime field $Z/pZ$.
background
The module supplies a minimal explicit surface for auditing elliptic-curve discrete-logarithm claims. It equips a finite carrier ZMod p, a short Weierstrass curve, points including infinity, the chord-tangent group operation, scalar multiplication, and an ECDLP solution predicate. ECPoint is the carrier type whose elements are later fed to onCurve, pointAdd and scalarMul. Upstream results supply identity functors and point intervals used in the broader foundation, but the local construction follows the standard Weierstrass model over a prime field.
proof idea
The declaration is an inductive definition with two constructors. Infinity is introduced as the identity element. Affine supplies the ordinary points over ZMod p. Deriving DecidableEq and Repr equips the type for equality testing and printing inside the watch harness.
why it matters
ECPoint is the foundational carrier for every subsequent definition in the module, including ECDLPInstance, onCurve, pointAdd, scalarMul and PublicECDLPData. It makes the ordinary mathematical ECDLP problem precise so that Recognition Science candidate invariants can be stated against concrete data rather than an abstract group. The construction fills the first step of the watch surface described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.