theorem Elligator1.q_ne_two (q : ℕ) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : q ≠ 2

theorem Elligator1.q_not_dvd_two {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : ¬q ∣ 2

theorem Elligator1.two_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : 2 ≠ 0

theorem Elligator1.q_sub_one_over_two_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : (q - 1) / 2 ≠ 0

noncomputable def Elligator1.χ {F : Type u_1} [Field F] [Fintype F] (a : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : F

χ(a) is the quadratic character of a in the finite field F with q elements, where q is a prime congruent to 3 modulo 4.

This function was added, since Mathlib.NumberTheory.LegendreSymbol.Basic is restricted to ℤ.

Paper definition at chapter 3.1.

Equations

• Elligator1.χ a q field_cardinality q_prime q_mod_4_congruent_3 = a ^ ((Fintype.card F - 1) / 2)

theorem Elligator1.χ_a_zero_eq_zero {F : Type u_1} [Field F] [Fintype F] (a : F) (a_eq_zero : a = 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a = 0

theorem Elligator1.χ_a_ne_zero {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a ≠ 0

theorem Elligator1.neg_χ_a_ne_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a ≠ -χ_of_a

theorem Elligator1.χ_a_eq_one {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (a_square : IsSquare a) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a = 1

theorem Elligator1.χ_of_a_pow_n_eq_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (n : ↑{n : ℕ | Odd n}) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a ^ ↑n = χ_of_a

theorem Elligator1.χ_of_a_eq_neg_one {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (a_nonsquare : IsSquare a = (false = true)) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a = -1

theorem Elligator1.χ_of_neg_one_eq_neg_one {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_neg_one := χ (-1) q field_cardinality q_prime q_mod_4_congruent_3; χ_of_neg_one = -1

theorem Elligator1.χ_of_χ_of_a_eq_χ_of_a {F : Type u_1} [Field F] [Fintype F] (a : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; have χ_of_χ_of_a := χ χ_of_a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_χ_of_a = χ_of_a

theorem Elligator1.χ_of_a_mul_b_eq_χ_of_a_mul_χ_of_b {F : Type u_1} [Field F] [Fintype F] (a b : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; have χ_of_b := χ b q field_cardinality q_prime q_mod_4_congruent_3; have χ_of_a_mul_b := χ (a * b) q field_cardinality q_prime q_mod_4_congruent_3; χ_of_a_mul_b = χ_of_a * χ_of_b

theorem Elligator1.χ_of_one_over_a_eq_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_non_zero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_1_over_a := χ (1 / a) q field_cardinality q_prime q_mod_4_congruent_3; have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_1_over_a = χ_of_a

theorem Elligator1.χ_of_one_over_a_eq_one_over_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_non_zero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_1_over_a := χ (1 / a) q field_cardinality q_prime q_mod_4_congruent_3; have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; χ_of_1_over_a = 1 / χ_of_a

theorem Elligator1.one_over_χ_of_a_eq_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have χ_of_a := χ a q field_cardinality q_prime q_mod_4_congruent_3; 1 / χ_of_a = χ_of_a

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 : Nat.Prime 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 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 : Nat.Prime 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 : Nat.Prime 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] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : F

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

Paper definition at chapter 3.2 theorem 1.

Equations

• Elligator1.u t = (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 : Nat.Prime 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 : Nat.Prime 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 : Nat.Prime 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 : Nat.Prime 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 : Nat.Prime 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; c_of_s ≠ 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 : Nat.Prime 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 : Nat.Prime 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; c_of_s ≠ -1

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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; ¬∃ (w : F), w ^ 2 = 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] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : u t ≠ 0

theorem Elligator1.u_defined {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : ∃ (w : F), w = u t

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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : v t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 ≠ 0

theorem Elligator1.v_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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : ∃ (w : F), w = v t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3

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 : Nat.Prime 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 q_mod_4_congruent_3; X_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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : ∃ (w : F), w = X t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3

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 : Nat.Prime 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 q_mod_4_congruent_3; Y_of_t ≠ 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : ∃ (w : F), w = Y t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3

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 : Nat.Prime 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 q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : ∃ (w : F), w = x t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3

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 : Nat.Prime 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 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 : Nat.Prime 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 q_mod_4_congruent_3; x_of_t ≠ 0

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 : Nat.Prime 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 q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; r_of_s * X_of_t + (1 + X_of_t) ^ 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 : Nat.Prime 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 q_mod_4_congruent_3; y_of_t + 1 ≠ 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : ∃ (w : F), w = y t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3

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 : Nat.Prime 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 q_mod_4_congruent_3; have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime 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

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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; u t * v_of_t * X_of_t * Y_of_t * x_of_t * (y_of_t + 1) ≠ 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime 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

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 : Nat.Prime 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.ϕ_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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t ↔ ¬∃ (w : F) (_ : w ≠ -t), ϕ w s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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.

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 : Nat.Prime 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 q_mod_4_congruent_3 }) : Prop

Equations

• Elligator1.ϕ_over_F_prop1 s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 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 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 : Nat.Prime 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 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 : Nat.Prime 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 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 : Nat.Prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : (∀ (h : ↑point ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3), ϕ_over_F_prop1 s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 ⟨↑point, h⟩ ∧ ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 ⟨↑point, h⟩ ∧ ϕ_over_F_prop3 s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 ⟨↑point, h⟩) ↔ ↑point ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3; have ϕ_over_F_q_of_s := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : have E_over_F_of_s := E_over_F s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) (h : ↑point ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 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 : Nat.Prime 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 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 : Nat.Prime 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 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : ∃ (w : F), w = X2 s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : ∃ (w : F), w = z s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : ∃ (w : F), w = u2 s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : ∃ (w : F), w = t2 s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 q_mod_4_congruent_3 }) : have t2_of_point := t2 s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 point; have ϕ_of_t2_of_point := ϕ t2_of_point s s_h1 s_h2 q field_cardinality q_prime 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 : ℕ) : ℕ

Equations

• Elligator1.b q = ⌊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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (τ : { n : List Binary // n ∈ S (b q) }) : F

Equations

• Elligator1.σ q field_cardinality q_prime q_mod_4_congruent_3 τ = ∑ i ∈ Finset.range (Elligator1.b q - 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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (τ : { n : List Binary // n ∈ S (b q) }) : 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 : ℕ) : (S (b q)).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 : Nat.Prime q) (q_mod_4_congruent_3 : q % 4 = 3) (τ₁ τ₂ : { n : List Binary // n ∈ S (b q) }) : ι s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3 τ₁ = ι s s_h1 s_h2 q field_cardinality q_prime 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 : Nat.Prime 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 : Nat.Prime 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 q_mod_4_congruent_3; have ι_S_of_s := ι_S s s_h1 s_h2 q field_cardinality q_prime q_mod_4_congruent_3; ϕ_over_F_of_s = ι_S_of_s