Documentation

Elligator.Elligator1.phiProperties

source
theorem Elligator.Elligator1.x_y_eq_zero_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) (x_eq_zero : (↑point).1 = 0) :
↑point = (0, 1)
source
theorem Elligator.Elligator1.y_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) (x_ne_zero : (↑point).1 ≠ 0) :
have y := (↑point).2; y ≠ 1
source
theorem Elligator.Elligator1.η_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 // 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) (x_ne_zero : (↑point).1 ≠ 0) :
have η_of_point := η q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; η_of_point ≠ 0
source
theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t_base_case {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 ϕ_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
source
theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t_main_case {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 ϕ_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
source
theorem Elligator.Elligator1.ϕ_of_t_eq_ϕ_of_neg_t {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
source
theorem Elligator.Elligator1.ϕ_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); ¬∃ (p : { n : F // n ≠ t ∧ n ≠ -t }), ↑(ϕ (↑p) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3) = ϕ_of_t
source
theorem Elligator.Elligator1.ϕ_of_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 ϕ_of_zero := ↑(ϕ 0 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 χ_of_c_of_s := LegendreSymbol.χ c_of_s 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; ϕ_of_zero = (2 * (c_of_s - 1) * s * χ_of_c_of_s / r_of_s, (r_of_s - 4) / (r_of_s + 4))
source
theorem Elligator.Elligator1.x_y_eq_ϕ_of_zero_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 x := (↑point).1; have y := (↑point).2; have X2_of_point := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have ϕ_of_zero := ϕ 0 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X2_of_point = 1 → ↑ϕ_of_zero = (x, y)
source
theorem Elligator.Elligator1.x_y_eq_ϕ_of_t_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) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) :
have x := (↑point).1; have y := (↑point).2; have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X ≠ 1 → ↑ϕ_of_t = (x, y)
source
theorem Elligator.Elligator1.ϕ_of_t2_eq_x_y_base_case {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 point := ↑(ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); have t' := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point; have ϕ_of_t' := ↑(ϕ t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); ϕ_of_t' = (0, 1)
source
theorem Elligator.Elligator1.ϕ_of_t2_eq_x_y_main_case {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 t' := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have ϕ_of_t' := ϕ 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; ↑ϕ_of_t' = (x_of_t, y_of_t)
source
theorem Elligator.Elligator1.ϕ_of_one_eq_zero_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 ϕ_of_one := ↑(ϕ 1 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); ϕ_of_one = (0, 1)
source
theorem Elligator.Elligator1.ϕ_of_neg_one_eq_zero_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 ϕ_of_neg_one := ↑(ϕ (-1) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); ϕ_of_neg_one = (0, 1)
source
theorem Elligator.Elligator1.ϕ_of_one_in_ϕ_of_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 ϕ_of_one := ↑(ϕ 1 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); ϕ_of_one ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3
source
theorem Elligator.Elligator1.point_in_ϕ_over_F_base_case {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) (x_eq_zero : (↑point).1 = 0) :
have ϕ_over_F := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ↑point ∈ ϕ_over_F
source
theorem Elligator.Elligator1.point_in_ϕ_over_F_main_case_with_y_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 // 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) (x_ne_zero : (↑point).1 ≠ 0) (y_eq_one : (↑point).2 = 1) :
have ϕ_over_F := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ↑point ∈ ϕ_over_F
source
theorem Elligator.Elligator1.point_in_ϕ_over_F_main_case_with_y_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) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) :
have ϕ_over_F := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ↑point ∈ ϕ_over_F
source
theorem Elligator.Elligator1.point_in_ϕ_over_F_main_case {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) (x_ne_zero : (↑point).1 ≠ 0) :
have ϕ_over_F := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ↑point ∈ ϕ_over_F
source
theorem Elligator.Elligator1.point_in_ϕ_over_F_of_point_props {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 }) :
ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point → ↑point ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3