Theorem related to the exceptional points in the birational mapping.
Theorem
ecurve::montgomery-only-point-with-y-0-when-aa-minus-4-non-square
limits certain exceptional points in the birational mapping
under a certain condition on the Montgomery curve.
Here we show that Jubjub, in Montgomery form,
satisfies that condition, i.e. that
Theorem:
(defthm not-pfield-squarep-of-jubjub-montgomery-a-square-minus-4 (b* ((a (ecurve::montgomery-curve->a (jubjub-montgomery-curve))) (a^2-4 (sub (mul a a (jubjub-q)) 4 (jubjub-q)))) (not (ecurve::pfield-squarep a^2-4 (jubjub-q)))))