v Variable Properties

In this file we introduce some generally helpful lemmas for v as introduced in Elligator.Elligator1.Variables.

References

See [bernstein2013a], Section 3.2, Theorem 1.

theorem Elligator.Elligator1.v_factored {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have v := v t s; have c := c s; have u := u t; v = u * (u ^ 2 + c ^ 2) * (u ^ 2 + 1 / c ^ 2)

theorem Elligator.Elligator1.v_factored_second_factor_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : u t ^ 2 + c s ^ 2 ≠ 0

theorem Elligator.Elligator1.v_factored_third_factor_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : u t ^ 2 + 1 / c s ^ 2 ≠ 0

theorem Elligator.Elligator1.v_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : v t s ≠ 0

theorem Elligator.Elligator1.χ_of_v_mul_v_of_t_pow_q_add_one_div_four_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} [DecidableEq F] (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have v := v t s; (LegendreSymbol.χ v * v) ^ ((q + 1) / 4) ≠ 0

theorem Elligator.Elligator1.v_comparison {F : Type u_1} [Field F] {s : F} (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have u1 := u t; have v2 := v ⟨t2, ⋯⟩ s; have r := r s; v2 = 1 / u1 ^ 5 + (r ^ 2 - 2) * 1 / u1 ^ 3 + 1 / u1

theorem Elligator.Elligator1.v_comparison_implication1 {F : Type u_1} [Field F] {s : F} (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have u1 := u t; have v1 := v t s; have v2 := v ⟨t2, ⋯⟩ s; v2 * u1 ^ 6 = v1

theorem Elligator.Elligator1.v_comparison_implication2 {F : Type u_1} [Field F] {s : F} (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have u1 := u t; have v1 := v t s; have v2 := v ⟨t2, ⋯⟩ s; v2 = v1 / u1 ^ 6

theorem Elligator.Elligator1.v_comparison_implication3 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : LegendreSymbol.χ (u t ^ 6) = 1

theorem Elligator.Elligator1.v_comparison_implication4 {F : Type u_1} [Field F] [Fintype F] {s : F} [DecidableEq F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have v1 := v t s; have v2 := v ⟨t2, ⋯⟩ s; LegendreSymbol.χ v2 = LegendreSymbol.χ v1

@[simp]

theorem Elligator.Elligator1.v_of_zero {F : Type u_1} [Field F] {s : F} : have v := v ⟨0, ⋯⟩ s; v = r s ^ 2