neg
plain-language theorem explainer
Negation on elliptic curve points over ZMod p is defined by cases: infinity remains fixed while affine points flip the sign of their y-coordinate. Cryptographers formalizing ECDLP instances in Lean would reference this when verifying the group axioms. The implementation matches the standard Weierstrass negation rule directly on the inductive ECPoint type.
Claim. For each natural number $p$, the map $neg : ECPoint p → ECPoint p$ sends the point at infinity to itself and the affine point $(x, y)$ to $(x, -y)$, where $ECPoint p$ is the inductive carrier consisting of infinity together with pairs in $ZMod p × ZMod p$.
background
The ECDLP Watch Surface module constructs an explicit finite model for elliptic curve discrete logarithm problems to test Recognition Science invariants. It introduces the inductive type ECPoint p with two constructors: infinity and affine x y where x and y lie in ZMod p. This point set will carry the chord-and-tangent group law once negation, addition, and scalar multiplication are supplied.
proof idea
The definition is given directly by pattern matching on the two constructors of ECPoint. Infinity maps to infinity. An affine point (x, y) maps to the affine point (x, -y), where the second-coordinate negation is taken from the imported field negation on ZMod p.
why it matters
This supplies the additive inverse required for the elliptic curve group law inside the ECDLPInstance predicate. It therefore participates in the formal surface used to audit candidate invariants from the Recognition framework against concrete cryptographic hardness assumptions. Downstream, analogous negation maps appear in the PhiRing and RecognitionCategory constructions that embed the golden ratio algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.