u2 Properties

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

References

See [bernstein2013a], Section 3.

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

theorem Elligator.Elligator1.u2_eq_u {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (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) (X_h : have P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have X := X t s; have X2 := X2 s P q; X2 = X) : have P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have u := u t; have u2 := u2 s P q; u2 = u

theorem Elligator.Elligator1.u2_eq_u' {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (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) (X_h : have P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have X' := X ⟨-↑t, ⋯⟩ s; have X2 := X2 s P q; X2 = X') : have t_h := ⋯; have P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have u' := u ⟨-↑t, t_h⟩; have u2 := u2 s P q; u2 = u'

theorem Elligator.Elligator1.u2_h1 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (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 t_h := ⋯; have u' := u ⟨-↑t, t_h⟩; have u := u t; have u2 := u2 s (↑P) q; u2 = u ∨ u2 = u'

theorem Elligator.Elligator1.one_add_u2_ne_zero_main_case {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 P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have u2 := u2 s P q; 1 + u2 ≠ 0

The key step: rewriting 1 + u2(ϕ(t)) in the main case (t ≠ ±1) to show it is ne_zero, using u2_h1 which gives u2 = u(t) or u2 = u(-t).

theorem Elligator.Elligator1.one_add_u2_ne_zero_base_case {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 P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have u2 := u2 s P q; 1 + u2 ≠ 0

theorem Elligator.Elligator1.one_add_u2_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) (P : { p : F × F // p ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod }) : have u2 := u2 s (↑P) q; 1 + u2 ≠ 0

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

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

Equations

• Elligator.Elligator1.u' sq_ne_pm_two hq_card hq_mod P = Elligator.Elligator1.z' sq_ne_pm_two hq_card hq_mod P * Elligator.Elligator1.X2 s (↑P) q

theorem Elligator.Elligator1.u'_pow_two_eq_X_pow_two {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have u := u' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; u ^ 2 = X ^ 2

theorem Elligator.Elligator1.u'_eq_X2_or_u'_eq_neg_X2 {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have u := u' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; u = X ∨ u = -X

theorem Elligator.Elligator1.u'_ne_neg_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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have u := u' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; X ≠ 1 → u ≠ -1

theorem Elligator.Elligator1.one_add_u'_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) (P : { p : F × F // p ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have u := u' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; X ≠ 1 → 1 + u ≠ 0

theorem Elligator.Elligator1.u'_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) (P : { p : F × F // p ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have u := u' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; X ≠ 1 → u ≠ 0

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator.Elligator1.v'_eq_z'_mul_Y'_pow_two {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_ne_one : (↑P).2 ≠ 1) : have z := z' sq_ne_pm_two hq_card hq_mod P; have Y := Y' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have X := X2 s (↑P) q; X ≠ 1 → v = z * Y ^ 2

theorem Elligator.Elligator1.v'_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) (P : { p : F × F // p ∈ EOverF sq_ne_pm_two hq_card hq_mod }) (P_props : ϕOverFProps s ↑P) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have v := v' sq_ne_pm_two hq_card hq_mod P; X ≠ 1 → v ≠ 0

theorem Elligator.Elligator1.χ_of_v'_eq_χ_of_z' {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have z := z' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have χ_of_v := LegendreSymbol.χ v; have χ_of_z := LegendreSymbol.χ z; X ≠ 1 → χ_of_v = χ_of_z

theorem Elligator.Elligator1.χ_of_z'_eq_z' {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 }) : have X := X2 s (↑P) q; have z := z' sq_ne_pm_two hq_card hq_mod P; have χ_of_z := LegendreSymbol.χ z; X ≠ 1 → χ_of_z = z

theorem Elligator.Elligator1.χ_of_v'_eq_z' {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have v := v' sq_ne_pm_two hq_card hq_mod P; have z := z' sq_ne_pm_two hq_card hq_mod P; have χ_of_v := LegendreSymbol.χ v; X ≠ 1 → χ_of_v = z

theorem Elligator.Elligator1.X'_eq_χ_of_v'_mul_u' {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have v := v' sq_ne_pm_two hq_card hq_mod P; have u := u' sq_ne_pm_two hq_card hq_mod P; have χ_of_v := LegendreSymbol.χ v; X ≠ 1 → X = χ_of_v * u

theorem Elligator.Elligator1.Y'_pow_two_eq_χ_of_v'_mul_v' {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have Y := Y' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have χ_of_v := LegendreSymbol.χ v; X ≠ 1 → Y ^ 2 = χ_of_v * v

theorem Elligator.Elligator1.χ_of_v'_eq_z'_unfold_of_X'_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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have Y := Y' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have χ_of_v := LegendreSymbol.χ v; have c := c s; have term := Y * (X ^ 2 + 1 / c ^ 2); have χ_term := LegendreSymbol.χ term; X ≠ 1 → χ_of_v = χ_term

theorem Elligator.Elligator1.χ_of_v'_eq_χ_Y'_mul_u'_pow_two_add_one_div_c_pow_two {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have Y := Y' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have u := u' sq_ne_pm_two hq_card hq_mod P; have c := c s; X ≠ 1 → LegendreSymbol.χ v = LegendreSymbol.χ (Y * (u ^ 2 + 1 / c ^ 2))

theorem Elligator.Elligator1.u'_pow_two_add_one_div_c_pow_two_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) (P : { p : F × F // p ∈ EOverF sq_ne_pm_two hq_card hq_mod }) : have u := u' sq_ne_pm_two hq_card hq_mod P; have c := c s; u ^ 2 + 1 / c ^ 2 ≠ 0

theorem Elligator.Elligator1.Y'_observation1 {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have Y := Y' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have u := u' sq_ne_pm_two hq_card hq_mod P; have c := c s; X ≠ 1 → LegendreSymbol.χ Y = LegendreSymbol.χ v * LegendreSymbol.χ (u ^ 2 + 1 / c ^ 2)

theorem Elligator.Elligator1.Y'_observation2 {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) (x_ne_zero : (↑P).1 ≠ 0) (y_ne_one : (↑P).2 ≠ 1) : have X := X2 s (↑P) q; have Y := Y' sq_ne_pm_two hq_card hq_mod P; have v := v' sq_ne_pm_two hq_card hq_mod P; have u := u' sq_ne_pm_two hq_card hq_mod P; have c := c s; X ≠ 1 → Y = (LegendreSymbol.χ v * v) ^ ((q + 1) / 4) * LegendreSymbol.χ v * LegendreSymbol.χ (u ^ 2 + 1 / c ^ 2)