		Search-engine friendly clone of the ACL2 documentation.

Jubjub-r-properties

Jubjub-r-doubling-injectivity

Injectivity of doubling in jubjub-r-pointp.

This is proved by cases on whether the points are zero or not. The case in which they are both non-zero is the more complicated one:

Assume 2P = 2Q.
Since P and Q have order r, we have rP = O = rQ.
Since r is odd, r = 2k+1 for some integer k.
So from the equality at (2) we have k(2P)+P = (2k+1)P = (2k+1)Q = k(2Q)+Q.
From the equality at (1), we also have k(2P) = k(2Q) and we can thus cancel them in the equality at (4), obtaining P = Q.

Definitions and Theorems

Theorem: jubjub-r-doubling-injectivity

(defthm jubjub-r-doubling-injectivity
  (implies (and (ecurve::twisted-edwards-add-associativity)
                (jubjub-r-pointp x)
                (jubjub-r-pointp y))
           (equal (equal (jubjub-mul 2 x)
                         (jubjub-mul 2 y))
                  (equal x y))))