Montgomery-only-point-with-y-0-when-aa-minus-4-non-square
Theorem about the only point with zero ordinate
for certain Montgomery curves.
If A^2 - 4 is not a square,
then (0,0) is the only point on a Montgomery curve
with y = 0.
The proof is carried out via a series of lemmas
that explain it.
It requires some algebraic manipulations that are not simplifications;
thus, it would be interesting to see whether and how it is possible
to carry out the proofs more automatically
via sufficiently general rules.
This theorem has some significance, in particular, for the birational equivalence between
Montgomery and twisted Edwards curves: points with y = 0 on a Montgomery curve
are not amenable to the rational mapping,
because they make a denominator zero;
thus, they have to be treated specially for the mapping.
This theorem, under the aforementioned condition on A,
tells us that there is just one such point.
Definitions and Theorems
Theorem: montgomery-only-point-with-y-0-when-aa-minus-4-non-square
(defthm montgomery-only-point-with-y-0-when-aa-minus-4-non-square
(b* ((p (montgomery-curve->p curve))
(a (montgomery-curve->a curve))
(x (point-finite->x point)))
(implies (and (not (pfield-squarep (sub (mul a a p) 4 p)
p))
(not (equal (point-kind point) :infinite))
(equal (point-finite->y point) 0))
(equal (point-on-montgomery-p point curve)
(equal x 0)))))