theorem
Elligator.Elligator1.v_h1_third_factor_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 })
:
theorem
Elligator.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 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
Elligator.Elligator1.v_h1_second_factor_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 })
:
theorem
Elligator.Elligator1.χ_of_v_mul_v_of_t_pow_q_add_one_over_four_ne_zero
{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)
:
theorem
Elligator.Elligator1.v_comparison
{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 u1 := u t 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
Elligator.Elligator1.v_comparison_implication1
{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 u1 := u t q field_cardinality q_prime_power q_mod_4_congruent_3;
have v1 := v t 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
Elligator.Elligator1.v_comparison_implication2
{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)
:
let t1 := ↑t;
let t2 := -t1;
have h2_2 := ⋯;
have u1 := u t q field_cardinality q_prime_power q_mod_4_congruent_3;
have v1 := v t 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
Elligator.Elligator1.v_comparison_implication3
{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)
:
have u1 := u t 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
Elligator.Elligator1.v_comparison_implication4
{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)
:
let t1 := ↑t;
let t2 := -t1;
have h2_2 := ⋯;
have u1 := u t q field_cardinality q_prime_power q_mod_4_congruent_3;
have v1 := v t 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