		Search-engine friendly clone of the ACL2 documentation.

Jubjub-r-properties

Point-0-m1

The point (0,-1).

Signature
(point-0-m1) → *

This point is not in jubjub-r-pointp, because it is not zero and doubling it yields zero (so it cannot have order jubjub-r). This point plays a role in the proofs of other properties about jubjub-r-pointp.

This is part of Theorem 5.4.3 in [ZPS].

Definitions and Theorems

Function: point-0-m1

(defun point-0-m1 nil
  (declare (xargs :guard t))
  (let ((__function__ 'point-0-m1))
    (declare (ignorable __function__))
    (ecurve::point-finite 0 (1- (jubjub-q)))))

Theorem: point-0-m1-not-zero

(defthm point-0-m1-not-zero
  (not (equal (point-0-m1)
              (twisted-edwards-zero))))

Theorem: 2-point-0-m1-is-zero

(defthm 2-point-0-m1-is-zero
  (equal (jubjub-mul 2 (point-0-m1))
         (twisted-edwards-zero)))

Theorem: point-0-m1-not-in-jubjub-r

(defthm point-0-m1-not-in-jubjub-r
  (not (jubjub-r-pointp (point-0-m1))))