Inverted Map

This file collects the three conclusions of Theorem 3 in the Elligator paper. It describes the preimage and image of ϕ, and verifies the paper's explicit inverse formula on that image.

Main results

• ϕ_of_t_eq_ϕ_of_neg_t_iff_ϕ_preimages: the preimage of ϕ t consists exactly of t and -t; in particular, ϕ t = ϕ (-t) and there are no other preimages.
• props_iff_mem_ϕOverF: membership in the image ϕ(F) is equivalent to the three algebraic point conditions stated in part 2 of Theorem 3.
• X2_defined, z_defined, t2_defined: the denominators required by the inverse construction are nonzero on ϕ(F).
• ϕ_of_t2_eq_x_y: applying ϕ to the reconstructed parameter t2 recovers the original point.

References

See [bernstein2013a] Section 3.3, Theorem 3.

theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t_iff_ϕ_preimages {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : F) (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have ϕ_of_t := ↑(ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod); have ϕ_of_neg_t := ↑(ϕ (-t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); ϕ_of_t = ϕ_of_neg_t ↔ ¬∃ (p : { n : F // n ≠ t ∧ n ≠ -t }), ↑(ϕ (↑p) hs_ne_zero sq_ne_pm_two hq_card hq_mod) = ϕ_of_t

The preimage of ϕ t consists exactly of the two field elements t and -t.

This is part 1 of Theorem 3. The left side records ϕ t = ϕ (-t); the right side says that no field element distinct from both t and -t maps to ϕ t.

theorem Elligator.Elligator1.props_iff_mem_ϕOverF {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : F) (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have P := ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod; ϕOverFProps s ↑P ↔ ↑P ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod

Characterization of the image of ϕ by the three conditions in part 2 of Theorem 3. For P = ϕ t, membership in ϕ(F) is equivalent to ϕOverFProps s P: y + 1 ≠ 0, (1 + ηr)² - 1 is a square, and the exceptional case ηr = -2 has the specified x-coordinate.

Note: Original statement does not read like an iff. Only the proof explanation makes this more concrete.

theorem Elligator.Elligator1.ϕ_of_t2_eq_x_y {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : F) (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have P := ↑(ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod); have x_of_t := P.1; have y_of_t := P.2; have t' := t2 s P q; have ϕ_of_t' := ↑(ϕ t' hs_ne_zero sq_ne_pm_two hq_card hq_mod); ϕ_of_t' = (x_of_t, y_of_t)

The explicit inverse formula in part 3 of Theorem 3 recovers a point in ϕ(F).

Starting with P = ϕ t, the definitions X2, z, u2, and t2 reproduce the paper's quantities X2, z, u2, and t2; evaluating ϕ (t2 s P q) returns the coordinates of P.

theorem Elligator.Elligator1.X2_defined {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { p : F × F // p ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod }) : have y := (↑P).2; 2 * (y + 1) ≠ 0

The denominator 2 * (y + 1) in the inverse construction is nonzero on ϕ(F). This supplies the definedness of η, and hence of X2, in part 3 of Theorem 3.

theorem Elligator.Elligator1.z_defined {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : c s ^ 2 ≠ 0

The denominator c² occurring in the definition of z is nonzero.

theorem Elligator.Elligator1.t2_defined {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { p : F × F // p ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod }) : have u2_of_P := u2 s (↑P) q; 1 + u2_of_P ≠ 0

The denominator 1 + u2 in the reconstructed parameter t2 is nonzero on ϕ(F).