y Variable Properties

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

References

See [bernstein2013a], Section 3.2, Theorem 1.

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

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

theorem Elligator.Elligator1.y_add_one_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq 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 y := y t s; y + 1 ≠ 0

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

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