|
|
|---|
|
|
|
|---|
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:
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.