pith. machine review for the scientific record. sign in
def definition def or abbrev high

neg

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  43def neg {p : ℕ} : ECPoint p → ECPoint p
  44  | ECPoint.infinity => ECPoint.infinity
  45  | ECPoint.affine x y => ECPoint.affine x (-y)
  46
  47instance {p : ℕ} : Neg (ECPoint p) where
  48  neg := neg

proof body

Definition body.

  49
  50/-- Chord slope for two distinct affine x-coordinates. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.