		Search-engine friendly clone of the ACL2 documentation.

Curve-parameterization

Curve-zero

Neutral point of the subgroup.

Signature
(curve-zero curve) → zero
Arguments: curve — Guard (curvep curve).
Returns: zero — Type (curve-subgroupp zero curve).

This is the same as the neutral point of the curve, since the neutral point is shared with the subgroup.

Definitions and Theorems

Function: curve-zero

(defun curve-zero (curve)
  (declare (xargs :guard (curvep curve)))
  (declare (ignore curve))
  (let ((__function__ 'curve-zero))
    (declare (ignorable __function__))
    (ecurve::twisted-edwards-zero)))

Theorem: return-type-of-curve-zero

(defthm return-type-of-curve-zero
  (b* ((zero (curve-zero curve)))
    (curve-subgroupp zero curve))
  :rule-classes :rewrite)

Theorem: pointp-of-curve-zero

(defthm pointp-of-curve-zero
  (b* ((zero (curve-zero curve)))
    (pointp zero))
  :rule-classes :rewrite)

Theorem: curve-zero-of-curve-fix-curve

(defthm curve-zero-of-curve-fix-curve
  (equal (curve-zero (curve-fix curve))
         (curve-zero curve)))

Theorem: curve-zero-curve-equiv-congruence-on-curve

(defthm curve-zero-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (curve-zero curve)
                  (curve-zero curve-equiv)))
  :rule-classes :congruence)