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.Y_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} [DecidableEq F] (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 q; Y ≠ 0

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

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

theorem Elligator.Elligator1.Y_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; have Y1 := Y t s q; have Y2 := Y ⟨t2, ⋯⟩ s q; Y2 = Y1 / X1 ^ 3