X2 Variable Properties

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

References

See [bernstein2013a], Section 3.3, Theorem 3.

theorem Elligator.Elligator1.X2_eq_neg_one {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) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have X2 := X2 s (↑P) q; X2 = -1

theorem Elligator.Elligator1.X2_h1 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { P : F × F // ϕOverFProps s P }) : have η_of_P := η ↑P; have r := r s; have X2 := X2 s (↑P) q; (1 + η_of_P * r + X2) ^ 2 = (1 + η_of_P * r) ^ 2 - 1

theorem Elligator.Elligator1.X2_h2 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { P : F × F // ϕOverFProps s P }) : have η := η ↑P; have r := r s; have X2 := X2 s (↑P) q; X2 ^ 2 + 2 * (1 + η * r) * X2 + 1 = 0

theorem Elligator.Elligator1.X2_h3 {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) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : let t1 := ↑t; let t2 := -t1; have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have X' := X ⟨t2, ⋯⟩ s; have X := X t s; have X2 := X2 s (↑P) q; (X2 - X) * (X2 - X') = 0

theorem Elligator.Elligator1.X2_h4 {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) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : let t1 := ↑t; let t2 := -t1; have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have X' := X ⟨t2, ⋯⟩ s; have X := X t s; have X2 := X2 s (↑P) q; X2 = X ∨ X2 = X'

theorem Elligator.Elligator1.X2_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { P : F × F // ϕOverFProps s P }) : have X2 := X2 s (↑P) q; X2 ≠ 0

theorem Elligator.Elligator1.y_divisor_ne_zero_with_X2_for_X {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) (P : { P : F × F // ϕOverFProps s P }) : have r := r s; have X2 := X2 s (↑P) q; r * X2 + (1 + X2) ^ 2 ≠ 0

theorem Elligator.Elligator1.X2_ne_neg_one {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) (P : { P : F × F // ϕOverFProps s P }) (y_eq_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; X2 ≠ -1

theorem Elligator.Elligator1.X2_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) (P : { P : F × F // ϕOverFProps s P }) (y_ne_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; X2 + 1 ≠ 0

theorem Elligator.Elligator1.y_with_X2 {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) (P : { P : F × F // ϕOverFProps s P }) (y_eq_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; have r := r s; have y := (↑P).2; y = (r * X2 - (1 + X2) ^ 2) / (r * X2 + (1 + X2) ^ 2)

theorem Elligator.Elligator1.y_with_X2_of_X2_eq_one {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) (P : { P : F × F // ϕOverFProps s P }) (y_eq_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; have r := r s; have y := (↑P).2; X2 = 1 → y = (r - 4) / (r + 4)

theorem Elligator.Elligator1.η_mul_r_eq_neg_two_of_X2_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (P : { P : F × F // ϕOverFProps s P }) : have η := η ↑P; have X2 := X2 s (↑P) q; have r := r s; X2 = 1 → η * r = -2

theorem Elligator.Elligator1.X2_observation1_of_X2_ne_one {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) (P : { P : F × F // ϕOverFProps s P }) (y_eq_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; have y := (↑P).2; have r := r s; X2 ≠ 1 → (r * X2 + (1 + X2) ^ 2) ^ 2 * (1 - y ^ 2) = 4 * r * X2 * (1 + X2) ^ 2

theorem Elligator.Elligator1.X2_observation2_of_X2_ne_one {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) (P : { P : F × F // ϕOverFProps s P }) (y_eq_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; have y := (↑P).2; have r := r s; have d := d s; X2 ≠ 1 → (r * X2 + (1 + X2) ^ 2) ^ 2 * (1 - d * y ^ 2) = 2 * r / (r - 2) * (X2 ^ 4 + (r ^ 2 - 2) * X2 ^ 2 + 1)

theorem Elligator.Elligator1.one_sub_d_mul_y_pow_two_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq 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 // ϕOverFProps s P }) : have y := (↑P).2; have d := d s; 1 - d * y ^ 2 ≠ 0

theorem Elligator.Elligator1.x_pow_two_of_X2_ne_one_eq1 {F : Type u_1} [Field F] [Fintype F] [DecidableEq 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 }) (P_props : ϕOverFProps s ↑P) : have x := (↑P).1; have y := (↑P).2; have d := d s; x ^ 2 = (1 - y ^ 2) / (1 - d * y ^ 2)

theorem Elligator.Elligator1.x_pow_two_of_X2_ne_one_eq2_of_X2_ne_one {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) (P : { p : F × F // p ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (y_eq_one : (↑P).2 ≠ 1) : have x := (↑P).1; have X := X2 s (↑P) q; have r := r s; X ≠ 1 → x ^ 2 = 2 * (r - 2) * X ^ 2 * (1 + X) ^ 2 / (X ^ 5 + (r ^ 2 - 2) * X ^ 3 + X)

def Elligator.Elligator1.Y' {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 }) : F

Y' is the Y equivalent used in the proof reverse argumentation of Theorem 3 part C.

Equations

• Elligator.Elligator1.Y' sq_ne_pm_two hq_card hq_mod P = (Elligator.Elligator1.c s - 1) * s * Elligator.Elligator1.X2 s (↑P) q * (1 + Elligator.Elligator1.X2 s (↑P) q) / (↑P).1

theorem Elligator.Elligator1.Y'_pow_two_eq_of_X2_ne_one {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) (P : { p : F × F // p ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (y_eq_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have r := r s; have Y := Y' sq_ne_pm_two hq_card hq_mod P; X ≠ 1 → Y ^ 2 = X ^ 5 + (r ^ 2 - 2) * X ^ 3 + X

theorem Elligator.Elligator1.X2_ne_one_and_X2_ne_neg_one_of_X2_ne_one {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) (P : { P : F × F // ϕOverFProps s P }) (y_ne_one : (↑P).2 ≠ 1) : have X2 := X2 s (↑P) q; X2 ≠ 1 → X2 ≠ 1 ∧ X2 ≠ -1