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

theorem Elligator.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 Elligator.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 Elligator.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 Elligator.Elligator1.map_fulfills_helper_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 Elligator.Elligator1.variable_mul_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 Elligator.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; let d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have d_h := ⋯; edwards_curve_equation x_of_t y_of_t ⟨d_of_s, d_h⟩ q field_cardinality q_prime_power q_mod_4_congruent_3

noncomputable def Elligator.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) : { P : F × F // P ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }

Equations

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