ϕ Properties

In this file we introduce some generally helpful lemmas for ϕ.

References

See [bernstein2013a], Section 3.3.

theorem Elligator.Elligator1.x_y_eq_zero_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_eq_zero : (↑P).1 = 0) : ↑P = (0, 1)

theorem Elligator.Elligator1.y_ne_one {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (x_ne_zero : (↑P).1 ≠ 0) : have y := (↑P).2; y ≠ 1

theorem Elligator.Elligator1.η_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) : η ↑P ≠ 0

theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t_base_case {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { t : F // t = 1 ∨ t = -1 }) (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

theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t_main_case {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) (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

theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t {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

theorem Elligator.Elligator1.ϕ_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); ¬∃ (p : { n : F // n ≠ t ∧ n ≠ -t }), ↑(ϕ (↑p) hs_ne_zero sq_ne_pm_two hq_card hq_mod) = ϕ_of_t

theorem Elligator.Elligator1.eq_or_eq_neg_of_ϕ_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t 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) (h : ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod = ϕ t' hs_ne_zero sq_ne_pm_two hq_card hq_mod) : t = t' ∨ t = -t'

Equality of images under ϕ forces the inputs to agree up to sign. This is the preimage conclusion of Theorem 3, restated in the form needed for the injectivity argument in Theorem 4.

theorem Elligator.Elligator1.ϕ_of_zero {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) : have ϕ_of_zero := ↑(ϕ 0 hs_ne_zero sq_ne_pm_two hq_card hq_mod); have c := c s; have r := r s; ϕ_of_zero = (2 * (c - 1) * s * LegendreSymbol.χ c / r, (r - 4) / (r + 4))

theorem Elligator.Elligator1.x_y_eq_ϕ_of_zero_of_X2_eq_one {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 // ϕOverFProps s P }) (y_eq_one : (↑P).2 ≠ 1) : have x := (↑P).1; have y := (↑P).2; have X2_of_P := X2 s (↑P) q; have ϕ_of_zero := ϕ 0 hs_ne_zero sq_ne_pm_two hq_card hq_mod; X2_of_P = 1 → ↑ϕ_of_zero = (x, y)

theorem Elligator.Elligator1.x_y_eq_ϕ_of_t_of_X2_ne_one {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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have x := (↑P).1; have y := (↑P).2; have X := X2 s (↑P) q; have t := t' sq_ne_pm_two hq_card hq_mod P; have ϕ_of_t := ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod; X ≠ 1 → ↑ϕ_of_t = (x, y)

theorem Elligator.Elligator1.ϕ_of_t2_eq_x_y_base_case {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { n : F // n = 1 ∨ n = -1 }) (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 t' := t2 s P q; have ϕ_of_t' := ↑(ϕ t' hs_ne_zero sq_ne_pm_two hq_card hq_mod); ϕ_of_t' = (0, 1)

theorem Elligator.Elligator1.ϕ_of_t2_eq_x_y_main_case {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) (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 t' := t2 s (↑P) q; have ϕ_of_t' := ϕ t' hs_ne_zero sq_ne_pm_two hq_card hq_mod; have x_of_t := x t s q; have y_of_t := y t s; ↑ϕ_of_t' = (x_of_t, y_of_t)

theorem Elligator.Elligator1.ϕ_of_one_eq_zero_one {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) : have ϕ_of_one := ↑(ϕ 1 hs_ne_zero sq_ne_pm_two hq_card hq_mod); ϕ_of_one = (0, 1)

theorem Elligator.Elligator1.ϕ_of_neg_one_eq_zero_one {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) : have ϕ_of_neg_one := ↑(ϕ (-1) hs_ne_zero sq_ne_pm_two hq_card hq_mod); ϕ_of_neg_one = (0, 1)

theorem Elligator.Elligator1.ϕ_of_one_in_ϕ_of_F {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) : have ϕ_of_one := ↑(ϕ 1 hs_ne_zero sq_ne_pm_two hq_card hq_mod); ϕ_of_one ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod

theorem Elligator.Elligator1.P_in_ϕOverF_base_case {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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_eq_zero : (↑P).1 = 0) : have ϕOverF := ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod; ↑P ∈ ϕOverF

theorem Elligator.Elligator1.P_in_ϕOverF_main_case_with_y_eq_one {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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (x_ne_zero : (↑P).1 ≠ 0) (y_eq_one : (↑P).2 = 1) : have ϕOverF := ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod; ↑P ∈ ϕOverF

theorem Elligator.Elligator1.P_in_ϕOverF_main_case_with_y_ne_one {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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have ϕOverF := ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod; ↑P ∈ ϕOverF

theorem Elligator.Elligator1.P_in_ϕOverF_main_case {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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) : have ϕOverF := ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod; ↑P ∈ ϕOverF

theorem Elligator.Elligator1.P_in_ϕOverF_of_P_props {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 ∈ EOverF sq_ne_pm_two hq_card hq_mod }) : ϕOverFProps s ↑P → ↑P ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod