t2 Variable Properties

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

References

See [bernstein2013a], Section 3.3.

theorem Elligator.Elligator1.t2_eq_one {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 t2_of_P := t2 s (↑P) q; t2_of_P = 1

theorem Elligator.Elligator1.t2_eq_t {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 t2_of_P := t2 s (↑P) q; t2_of_P = ↑t

theorem Elligator.Elligator1.t2_eq_t' {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 t2_of_P := t2 s P q; have t' := -↑t; t2_of_P = t'

theorem Elligator.Elligator1.t2_in_t_or_neg_t {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : 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) : have P := ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod; have t' := -t; have t2_of_P := t2 s (↑P) q; t2_of_P = t ∨ t2_of_P = t'

def Elligator.Elligator1.t' {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

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

Equations

• Elligator.Elligator1.t' sq_ne_pm_two hq_card hq_mod P = (1 - Elligator.Elligator1.u' sq_ne_pm_two hq_card hq_mod P) / (1 + Elligator.Elligator1.u' sq_ne_pm_two hq_card hq_mod P)

theorem Elligator.Elligator1.t'_ne_one_and_t'_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) (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 t := t' sq_ne_pm_two hq_card hq_mod P; X ≠ 1 → t ≠ 1 ∧ t ≠ -1

theorem Elligator.Elligator1.one_add_t'_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 t := t' sq_ne_pm_two hq_card hq_mod P; X ≠ 1 → t + 1 ≠ 0

theorem Elligator.Elligator1.u'_eq_one_sub_t'_div_one_add_t' {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 u := u' sq_ne_pm_two hq_card hq_mod P; have t := t' sq_ne_pm_two hq_card hq_mod P; X ≠ 1 → u = (1 - t) / (1 + t)

theorem Elligator.Elligator1.u'_eq_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) (X_h : have X := X2 s (↑P) q; X ≠ 1) : have u' := u' sq_ne_pm_two hq_card hq_mod P; let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have u := u ⟨t, t_h⟩; u' = u

theorem Elligator.Elligator1.v'_eq_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) (X_h : have X := X2 s (↑P) q; X ≠ 1) : have v' := v' sq_ne_pm_two hq_card hq_mod P; let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have v := v ⟨t, t_h⟩ s; v' = v

theorem Elligator.Elligator1.X'_eq_X {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) (X_h : have X := X2 s (↑P) q; X ≠ 1) : have X' := X2 s (↑P) q; let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have X := X ⟨t, t_h⟩ s; X' = X

theorem Elligator.Elligator1.Y'_eq_Y {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) (X_h : have X := X2 s (↑P) q; X ≠ 1) : have Y' := Y' sq_ne_pm_two hq_card hq_mod P; let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have Y := Y ⟨t, t_h⟩ s q; Y' = Y

def Elligator.Elligator1.x' {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

x' is the x 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.x'_eq_x {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) (X_h : have X' := X2 s (↑P) q; X' ≠ 1) : let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have x := x ⟨t, t_h⟩ s q; have x' := x' sq_ne_pm_two hq_card hq_mod P; x' = 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

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

theorem Elligator.Elligator1.y'_eq_y {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) (X_h : have X' := X2 s (↑P) q; X' ≠ 1) : let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have y := y ⟨t, t_h⟩ s; have y' := y' sq_ne_pm_two hq_card hq_mod P; y' = y

theorem Elligator.Elligator1.x'_and_y'_fulfill_curve_equation {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) (X_h : have X' := X2 s (↑P) q; X' ≠ 1) : have x' := x' sq_ne_pm_two hq_card hq_mod P; have y' := y' sq_ne_pm_two hq_card hq_mod P; let d := d s; have d_h := ⋯; edwardsCurveEquation x' y' ⟨d, d_h⟩

theorem Elligator.Elligator1.y_eq_y_of_P {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) (X_h : have X' := X2 s (↑P) q; X' ≠ 1) : let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have y := y ⟨t, t_h⟩ s; have y_of_P := (↑P).2; y = y_of_P

theorem Elligator.Elligator1.x_eq_x_of_P {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) (X_h : have X' := X2 s (↑P) q; X' ≠ 1) : let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have x := x ⟨t, t_h⟩ s q; have x_of_P := (↑P).1; x = x_of_P

theorem Elligator.Elligator1.x_y_of_P_eq_x_y {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) (X_h : have X' := X2 s (↑P) q; X' ≠ 1) : let t := t' sq_ne_pm_two hq_card hq_mod P; have t_h := ⋯; have y := y ⟨t, t_h⟩ s; have y_of_P := (↑P).2; have x := x ⟨t, t_h⟩ s q; have x_of_P := (↑P).1; (x, y) = (x_of_P, y_of_P)