theorem Elligator.Elligator1.X2_eq_neg_one {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t = 1 ∨ t = -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 point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_point = -1

theorem Elligator.Elligator1.X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) : have η_of_point := η q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; (1 + η_of_point * r_of_s + X2_of_t) ^ 2 = (1 + η_of_point * r_of_s) ^ 2 - 1

theorem Elligator.Elligator1.X2_h2 {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 // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) : have η_of_point := η q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_t ^ 2 + 2 * (1 + η_of_point * r_of_s) * X2_of_t + 1 = 0

theorem Elligator.Elligator1.X2_h3 {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t ≠ 1 ∧ t ≠ -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) : let t1 := ↑t; let t2 := -t1; have h2_2 := ⋯; have point := ϕ (↑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 X'_of_t := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; (X2_of_t - X_of_t) * (X2_of_t - X'_of_t) = 0

theorem Elligator.Elligator1.X2_h4 {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t ≠ 1 ∧ t ≠ -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) : let t1 := ↑t; let t2 := -t1; have h2_2 := ⋯; have point := ϕ (↑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 X'_of_t := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_t = X_of_t ∨ X2_of_t = X'_of_t

theorem Elligator.Elligator1.X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_point ≠ 0

theorem Elligator.Elligator1.y_divisor_ne_zero_with_X2_for_X {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 // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; r_of_s * X2_of_point + (1 + X2_of_point) ^ 2 ≠ 0

theorem Elligator.Elligator1.X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_eq_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_point ≠ -1

theorem Elligator.Elligator1.X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_ne_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_point + 1 ≠ 0

theorem Elligator.Elligator1.y_with_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 // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_eq_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y := (↑point).2; y = (r_of_s * X2_of_point - (1 + X2_of_point) ^ 2) / (r_of_s * X2_of_point + (1 + X2_of_point) ^ 2)

theorem Elligator.Elligator1.y_with_X2_of_X2_eq_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_eq_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y := (↑point).2; X2_of_point = 1 → y = (r_of_s - 4) / (r_of_s + 4)

theorem Elligator.Elligator1.η_mul_r_eq_neg_two_of_X2_eq_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) : have η_of_point := η q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X2_of_point = 1 → η_of_point * r_of_s = -2

theorem Elligator.Elligator1.X2_observation1_of_X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_eq_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have y := (↑point).2; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X2_of_point ≠ 1 → (r_of_s * X2_of_point + (1 + X2_of_point) ^ 2) ^ 2 * (1 - y ^ 2) = 4 * r_of_s * X2_of_point * (1 + X2_of_point) ^ 2

theorem Elligator.Elligator1.X2_observation2_of_X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_eq_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have y := (↑point).2; have r_of_s := r 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; X2_of_point ≠ 1 → (r_of_s * X2_of_point + (1 + X2_of_point) ^ 2) ^ 2 * (1 - d_of_s * y ^ 2) = 2 * r_of_s / (r_of_s - 2) * (X2_of_point ^ 4 + (r_of_s ^ 2 - 2) * X2_of_point ^ 2 + 1)

theorem Elligator.Elligator1.one_sub_d_mul_y_pow_two_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) : have y := (↑point).2; have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; 1 - d_of_s * y ^ 2 ≠ 0

theorem Elligator.Elligator1.x_pow_two_of_X2_ne_one_eq1 {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 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) : have x := (↑point).1; have y := (↑point).2; have d := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x ^ 2 = (1 - y ^ 2) / (1 - d * y ^ 2)

theorem Elligator.Elligator1.x_pow_two_of_X2_ne_one_eq2_of_X2_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) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (y_eq_one : (↑point).2 ≠ 1) : have x := (↑point).1; have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X ≠ 1 → x ^ 2 = 2 * (r - 2) * X ^ 2 * (1 + X) ^ 2 / (X ^ 5 + (r ^ 2 - 2) * X ^ 3 + X)

noncomputable def Elligator.Elligator1.Y' {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 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) : F

Equations

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

theorem Elligator.Elligator1.Y'_pow_two_eq_of_X2_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) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (y_eq_one : (↑point).2 ≠ 1) : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have r := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; X ≠ 1 → Y ^ 2 = X ^ 5 + (r ^ 2 - 2) * X ^ 3 + X

theorem Elligator.Elligator1.X2_ne_one_and_X2_ne_neg_one_of_X2_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) (point : { P : F × F // ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 P }) (y_ne_one : (↑point).2 ≠ 1) : have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_point ≠ 1 → X2_of_point ≠ 1 ∧ X2_of_point ≠ -1