z Properties #

In this file we introduce some generally helpful lemmas for z as introduced in Elligator.Elligator1.Variables.

References #

See [bernstein2013a], Section 3.

theorem Elligator.Elligator1.z_eq_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} [DecidableEq F] (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 z := z s P q; z = 0

def Elligator.Elligator1.z' {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 }) :

z' is the z equivalent used in the proof reverse argumentation of Theorem 3 part C.

Equations

Instances For

theorem Elligator.Elligator1.Y'_ne_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) (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 Y := Y' sq_ne_pm_two hq_card hq_mod P; Y ≠ 0

theorem Elligator.Elligator1.X_pow_two_add_1_div_c_pow_two_ne_zero {F : Type u_1} [Field F] [Fintype 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 }) :

have X := X2 s (↑P) q; have c := c s; X ^ 2 + 1 / c ^ 2 ≠ 0

theorem Elligator.Elligator1.z'_argument_ne_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) (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 Y := Y' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; have c := c s; Y * (X ^ 2 + 1 / c ^ 2) ≠ 0

theorem Elligator.Elligator1.z'_ne_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) (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 z := z' sq_ne_pm_two hq_card hq_mod P; z ≠ 0

theorem Elligator.Elligator1.z'_eq_one_or_z'_eq_neg_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 z := z' sq_ne_pm_two hq_card hq_mod P; z = 1 ∨ z = -1