x Variable Properties

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

References

See [bernstein2013a], Section 3.2, Theorem 1.

theorem Elligator.Elligator1.x_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} [DecidableEq F] (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 x := x t s q; x ≠ 0

theorem Elligator.Elligator1.x_comparison {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) : let t1 := ↑t; let t2 := -t1; have x1 := x t s q; have x2 := x ⟨t2, ⋯⟩ s q; x2 = x1

theorem Elligator.Elligator1.x_y_eq_zero_sign_one {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { P : F × F // P ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (hx_eq_zero : (↑P).1 = 0) : ↑P = (0, 1) ∨ ↑P = (0, -1)