		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-zero

Neutral point of the twisted Edwards curve group.

Signature
(twisted-edwards-zero) → point
Returns: point — Type (pointp point).

This is always (0,1). See the paper referenced in twisted-edwards.

Definitions and Theorems

Function: twisted-edwards-zero

(defun twisted-edwards-zero nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'twisted-edwards-zero))
    (declare (ignorable acl2::__function__))
    (point-finite 0 1)))

Theorem: pointp-of-twisted-edwards-zero

(defthm pointp-of-twisted-edwards-zero
  (b* ((point (twisted-edwards-zero)))
    (pointp point))
  :rule-classes :rewrite)

Theorem: point-on-twisted-edwards-p-of-twisted-edwards-zero

(defthm point-on-twisted-edwards-p-of-twisted-edwards-zero
  (point-on-twisted-edwards-p (twisted-edwards-zero)
                              curve))