c Variable Properties

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

References

See [bernstein2013a], Section 3.2, Theorem 1.

theorem Elligator.Elligator1.c_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) : c s ≠ 0

theorem Elligator.Elligator1.c_ne_one {F : Type u_1} [Field F] {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : c s ≠ 1

theorem Elligator.Elligator1.c_sub_one_ne_zero {F : Type u_1} [Field F] {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : c s - 1 ≠ 0

theorem Elligator.Elligator1.c_ne_neg_one {F : Type u_1} [Field F] {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : c s ≠ -1

theorem Elligator.Elligator1.c_add_one_ne_zero {F : Type u_1} [Field F] {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : c s + 1 ≠ 0

theorem Elligator.Elligator1.c_mul_sub_one_mul_add_one_ne_zero {F : Type u_1} [Field F] [Fintype 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) : have c := c s; c * (c - 1) * (c + 1) ≠ 0

theorem Elligator.Elligator1.s_pow_two_eq_two_div_c {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : s ^ 2 = 2 / c s