ECPoint
plain-language theorem explainer
The declaration defines the set of points on a short Weierstrass elliptic curve over the finite field Z/pZ, consisting of the point at infinity together with affine pairs. Researchers testing Recognition Science invariants against elliptic-curve discrete-logarithm instances would cite this carrier when constructing explicit ECDLP surfaces. The definition is supplied directly as an inductive type with two constructors.
Claim. For a natural number $p$, the points on the elliptic curve consist of the distinguished point at infinity together with all pairs $(x,y)$ where $x,y$ lie in the prime field $Z/pZ$.
background
The module supplies a minimal, explicit surface for auditing elliptic-curve discrete-logarithm claims before any Recognition Science invariant is applied. It works with a finite carrier ZMod p, a short Weierstrass curve, the point at infinity as group identity, the chord-tangent addition law, scalar multiplication, and an ECDLP solution predicate. Upstream dependencies include the identity event from ObserverForcing (the canonical identity at J-cost minimum) and the identity functor from VantageCategory, which appear in the broader module context for strain and recognition structures.
proof idea
The declaration is an inductive definition with two constructors: infinity for the point at infinity and affine for pairs drawn from ZMod p. No lemmas or tactics are applied; the type is introduced directly.
why it matters
ECPoint supplies the point carrier used by ECDLPInstance, onCurve, pointAdd, scalarMul, and PublicECDLPData. It therefore anchors the ECDLP watch harness whose purpose is to keep later RS invariants honest by restricting them to public data only. The construction sits inside the cryptography domain of the Recognition Science mirror and prepares the ground for testing candidate invariants against the standard ECDLP formulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.