# Birational-montgomery-twisted-edwards

Birational equivalence between
Montgomery curves and twisted Edwards curves.

There is a birational equivalence between Montgomery curves and twisted Edwards curves, described in Section 3 of Bernstein, Birkner, Joye, Lange, and Peters's ``Twisted Edwards Curves''. That is, there are:

- A mapping between
the set of Montgomery curves
and the set of twisted Edwards curves.
- Given Montgomery and twisted Edwards curves related by the above mapping,
there is a mapping between
the set of points of one curve
and the set of points of the other curve.

Here `birational' means that the mappings
between the sets of points of two corresponding curves
are rational functions.
Their denominators are 0 only for a finite number of points of the curves;
the complete mappings can be therefore defined
via the rational formulas plus a few special explicit cases.

Here we define these mappings.
We plan to prove properties of them at some point.

In certain cases, these birational mappings may be scaled.
See for instance this page.
Thus, our ACL2 functions that define the mappings
take an additional scaling factor as argument.
This can be set to 1 for the non-scaled mappings.

### Subtopics

- Twisted-edwards-point-to-montgomery-point
- Map a point on a Twisted Edwards curve to
the corresponding point on the corresponding Montgomery curve.
- Montgomery-point-to-twisted-edwards-point
- Map a point on a Montgomery curve to
the corresponding point on the corresponding twisted Edwards curve.
- Montgomery-to-twisted-edwards
- Map a Montgomery curve to a twisted Edwards curve.
- Twisted-edwards-to-montgomery
- Map a twisted Edwards curve to a Montgomery curve.