noncomputable def Elligator1.c {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

c(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• Elligator1.c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = 2 / s ^ 2

noncomputable def Elligator1.r {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

r(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.d {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

d(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.u {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

u(t) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• Elligator1.u t q field_cardinality q_prime_power q_mod_4_congruent_3 = (1 - ↑t) / (1 + ↑t)

noncomputable def Elligator1.v {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

v(t, s) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.X {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

X(t, s) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.Y {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

Y(t, s) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.x {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

x(t, s) is a function defined in the paper. It is the x-coordinate of the point on the curve.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.y {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

y(t, s) is a function defined in the paper. It is the y-coordinate of the point on the curve.

Paper definition at chapter 3.2 theorem 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator1.c_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ≠ 0

theorem Elligator1.Y_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ^ 2 ≠ 0

theorem Elligator1.s_pow_two_ne_two {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : s ^ 2 ≠ 2

theorem Elligator1.s_pow_two_ne_neg_two {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : s ^ 2 ≠ -2

theorem Elligator1.c_ne_one {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ≠ 1

theorem Elligator1.c_ne_neg_one {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ≠ -1

theorem Elligator1.c_add_one_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s + 1 ≠ 0

theorem Elligator1.c_sub_one_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s - 1 ≠ 0

theorem Elligator1.c_h {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s * (c_of_s - 1) * (c_of_s + 1) ≠ 0

theorem Elligator1.r_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; r_of_s ≠ 0

theorem Elligator1.d_nonsquare {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ¬IsSquare d_of_s

theorem Elligator1.one_sub_t_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 - ↑t ≠ 0

theorem Elligator1.one_add_t_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 + ↑t ≠ 0

theorem Elligator1.u_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : u t q field_cardinality q_prime_power q_mod_4_congruent_3 ≠ 0

theorem Elligator1.χ_sum_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; u_of_t ^ 2 + 1 / c_of_s ^ 2 ≠ 0

theorem Elligator1.v_h1 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; v_of_t = u_of_t * (u_of_t ^ 2 + c_of_s ^ 2) * (u_of_t ^ 2 + 1 / c_of_s ^ 2)

theorem Elligator1.v_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v_of_t ≠ 0

theorem Elligator1.u_defined {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 + ↑t ≠ 0

theorem Elligator1.X_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X_of_t ≠ 0

theorem Elligator1.Y_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y_of_t ≠ 0

theorem Elligator1.X_mul_Y_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X_of_t * Y_of_t ≠ 0

theorem Elligator1.x_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ≠ 0

theorem Elligator1.one_add_X_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; 1 + X_of_t ≠ 0

theorem Elligator1.x_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x_of_t ≠ 0

theorem Elligator1.map_fulfills_specific_equation {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y_of_t ^ 2 = X_of_t ^ 5 + (r_of_s ^ 2 - 2) * X_of_t ^ 3 + X_of_t

theorem Elligator1.y_divisor_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; r_of_s * X_of_t + (1 + X_of_t) ^ 2 ≠ 0

theorem Elligator1.y_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 * X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 + (1 + X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3) ^ 2 ≠ 0

theorem Elligator1.y_add_one_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; y_of_t + 1 ≠ 0

theorem Elligator1.u_mul_v_mul_X_mul_Y_mul_x_mul_y_add_one_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; u_of_t * v_of_t * X_of_t * Y_of_t * x_of_t * (y_of_t + 1) ≠ 0

theorem Elligator1.map_fulfills_curve_equation {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x_of_t ^ 2 + y_of_t ^ 2 = 1 + d_of_s * x_of_t ^ 2 * y_of_t ^ 2

noncomputable def Elligator1.ϕ {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F × F

ϕ(t, s) is a function defined in the paper. It maps a numer t in F s to a point on the curve.

Paper definition at chapter 3.2 definition 2.

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator1.u_comparison {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have u2 := u ⟨t2, h2_2⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; u2 = 1 / u1

theorem Elligator1.v_comparison {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v2 = 1 / u1 ^ 5 + (r_of_s ^ 2 - 2) * 1 / u1 ^ 3 + 1 / u1

theorem Elligator1.v_comparison_implication1 {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v1 := v ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v2 * u1 ^ 6 = v1

theorem Elligator1.v_comparison_implication2 {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v1 := v ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v2 = v1 / u1 ^ 6

theorem Elligator1.v_comparison_implication3 {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; have t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_u1_pow_6 := LegendreSymbol.χ (u1 ^ 6) q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_u1_pow_6 = 1

theorem Elligator1.v_comparison_implication4 {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v1 := v ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_v1 := LegendreSymbol.χ v1 q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_v2 := LegendreSymbol.χ v2 q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_v2 = χ_of_v1

theorem Elligator1.X_comparison {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have X1 := X ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2 := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X2 = 1 / X1

theorem Elligator1.Y_comparison {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have X1 := X ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2 := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y1 := Y ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y2 := Y ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y2 = Y1 / X1 ^ 3

theorem Elligator1.x_comparison {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have x1 := x ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have x2 := x ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x2 = x1

theorem Elligator1.y_comparison {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have y1 := y ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y2 := y ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; y2 = y1

theorem Elligator1.ϕ_inv_only_two_specific_preimages_mp {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; (¬∃ (w : { n : F // n ≠ t ∧ n ≠ -t }), ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t) → ϕ_of_t = ϕ_of_neg_t

theorem Elligator1.ϕ_inv_only_two_specific_preimages_mpr {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t → ¬∃ (w : { n : F // n ≠ t ∧ n ≠ -t }), ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t

theorem Elligator1.ϕ_inv_only_two_specific_preimages {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t ↔ ¬∃ (w : { n : F // n ≠ t ∧ n ≠ -t }), ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t

def Elligator1.E_over_F {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : Set (F × F)

E_over_F(s, q) is the set of points on the curve defined by the equation in the paper.

Paper definition at chapter 3.3 theorem 3.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.ϕ_over_F_prop1 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : Prop

Equations

• Elligator1.ϕ_over_F_prop1 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point = ((↑point).2 + 1 ≠ 0)

noncomputable def Elligator1.η {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

η(s, q, point) is a function defined in the paper.

Paper definition at chapter 3.3 theorem 3.

Equations

• Elligator1.η s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point = ((↑point).2 - 1) / (2 * ((↑point).2 + 1))

def Elligator1.ϕ_over_F_prop2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : Prop

Equations

• One or more equations did not get rendered due to their size.

def Elligator1.ϕ_over_F_prop3 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : Prop

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.ϕ_over_F {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : Set (F × F)

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator1.point_in_E_over_F_with_props_iff_point_in_ϕ_over_F {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : (∀ (h : ↑point ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3), ϕ_over_F_prop1 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ⟨↑point, h⟩ ∧ ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ⟨↑point, h⟩ ∧ ϕ_over_F_prop3 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ⟨↑point, h⟩) ↔ ↑point ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3

theorem Elligator1.E_over_F_subset_ϕ_over_F {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have E_over_F_of_s := E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_over_F_q_of_s := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; E_over_F_of_s ⊆ ϕ_over_F_q_of_s

theorem Elligator1.point_in_E_over_F {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have E_over_F_of_s := E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ↑point ∈ E_over_F_of_s

noncomputable def Elligator1.X2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (h : ↑point ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3) : F

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.z {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.u2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Elligator1.t2 {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator1.X2_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : ∃ (w : F), w = X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point ⋯

theorem Elligator1.z_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : ∃ (w : F), w = z s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem Elligator1.u2_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : ∃ (w : F), w = u2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem Elligator1.t2_defined {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : ∃ (w : F), w = t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem Elligator1.invmap_representative {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have t2_of_point := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point; have ϕ_of_t2_of_point := ϕ t2_of_point s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t2_of_point = ↑point

invmap_representative is ...

Paper definition at chapter 3.3 Theorem 3.3.

noncomputable def Elligator1.b (q : ℕ) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : ℕ

Equations

• Elligator1.b q q_prime_power q_mod_4_congruent_3 = ⌊Real.logb 2 ↑q⌋.toNat

@[reducible, inline]

abbrev Elligator1.Binary : Type

Equations

• Elligator1.Binary = Fin 2

def Elligator1.S (b : ℕ) : Set (List Binary)

Equations

• Elligator1.S b = {n : List Elligator1.Binary | n.length = b}

noncomputable def Elligator1.σ {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (τ : { n : List Binary // n ∈ S (b q q_prime_power q_mod_4_congruent_3) }) : F

Equations

• Elligator1.σ q field_cardinality q_prime_power q_mod_4_congruent_3 τ = ∑ i ∈ Finset.range (Elligator1.b q q_prime_power q_mod_4_congruent_3 - 1), ↑↑(↑τ)[i]! * 2 ^ i

noncomputable def Elligator1.ι {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (τ : { n : List Binary // n ∈ S (b q q_prime_power q_mod_4_congruent_3) }) : F × F

`ιis the injective map that maps a binary stringτto a point on the curveE(F_q)`.

Paper definition at chapter 3.4 Theorem 4.

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator1.S_cardinality (q : ℕ) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : (S (b q q_prime_power q_mod_4_congruent_3)).ncard = (q + 1) / 2

theorem Elligator1.ι_injective_map {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (τ₁ τ₂ : { n : List Binary // n ∈ S (b q q_prime_power q_mod_4_congruent_3) }) : ι s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 τ₁ = ι s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 τ₂ → τ₁ = τ₂

noncomputable def Elligator1.ι_S {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : Set (F × F)

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator1.ι_S_eq_ϕ_over_F {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have ϕ_over_F_of_s := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ι_S_of_s := ι_S s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_over_F_of_s = ι_S_of_s