Group law for projective Edwards curves

I'm reading this paper and in section 4 the author proposes projective elliptic curves.

I have a doubt on why it is assumed implicitly that $$c = 1$$. This is done explicitely in the Mathematica computations but only implicitely in the paper when it defines:

$$z_1 \oplus_1 z_2 := \tau((\tau z_1) \oplus_0 z_2) = \Big(\frac{x_1y_1-x_2y_2}{x_2y_1-x_1y_2}, \frac{x_1y_1+x_2y_2}{x_1x_2+y_1y_2}\Big)$$

If you follow the definitions of $$\tau$$ and $$\oplus_0$$ in detail you would get instead:

$$z_1 \oplus_1 z_2 := \tau((\tau z_1) \oplus_0 z_2) = \Big(\frac{x_1y_1-c x_2y_2}{x_2y_1-c x_1y_2}, \frac{x_1y_1+cx_2y_2}{x_1x_2+y_1y_2}\Big)$$

The problem is that I'm trying to formalize this in a proof assistant and thus I aim to have as much generality as possible unless there is a good justification for setting $$c = 1$$.

• At the start of section 4.1 the author makes a change of variables (assuming he can take a square root of $c$, so maybe after extending the base field) to obtain a curve of the form $$e(x, y)=x^{2}+y^{2}-1-t^{2}x^{2}y^{2}$$ which is now a $c =1$ curve. The justification is therefore that every more general edwards curve is isomorphic to a $c=1$ curve after an extension and by writing down the group law on these curves we get a group law on all edwards curves by composing with this isomorphism, if we want to add points on general curves. I would guess this is the reason for the assumption. – Alex J Best Aug 4 at 23:22