Map Properties

In this file we introduce lemmas, which are directly derivable from the main results in Elligator.Elligator1.Map.

These results are mainly used for Theorem 3 proof part A, i.e. results only proofable right in between Theorem 1 and proof part B.

This hierarchy allows to have a linear dependence hierarchy without polluting major result files.

References

See [bernstein2013a], Section 3.

theorem Elligator.Elligator1.y_h1 {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 y := y t s; have r := r s; have X := X t s; X ^ 2 + (2 + r * (y - 1) / (y + 1)) * X + 1 = 0

theorem Elligator.Elligator1.y_h2 {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 r := r s; have X := X t s; have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have η := η ↑P; X ^ 2 + 2 * (1 + η * r) * X + 1 = 0

theorem Elligator.Elligator1.y_h3 {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 r := r s; have X := X t s; have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have η := η ↑P; X + 1 / X = -2 * (1 + η * r)

theorem Elligator.Elligator1.X_comparison_implication {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) : let t1 := ↑t; let t2 := -t1; have X1 := X t s; have X2 := X ⟨t2, ⋯⟩ s; have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have η_of_P := η ↑P; have r := r s; X1 + X2 = -2 * (1 + η_of_P * r)

theorem Elligator.Elligator1.X_comparison_implication2 {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) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : let t1 := ↑t; let t2 := -t1; have X1 := X t s; have X2 := X ⟨t2, ⋯⟩ s; X2 * X1 = 1

theorem Elligator.Elligator1.χ_IsSquare_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) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have v := v t s; IsSquare ((LegendreSymbol.χ v * v) ^ ((q + 1) / 4))

theorem Elligator.Elligator1.y_comparison {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have y1 := y t s; have y2 := y ⟨t2, ⋯⟩ s; y2 = y1

theorem Elligator.Elligator1.P_comparison {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) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : let t1 := ↑t; let t2 := -t1; have t_h := ⋯; have y1 := y t s; have y2 := y ⟨t2, t_h⟩ s; have x1 := x t s q; have x2 := x ⟨t2, t_h⟩ s q; (x1, y1) = (x2, y2)

theorem Elligator.Elligator1.X_η_h1 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : have X := X t s; (X - 1) ^ 2 = 0

theorem Elligator.Elligator1.X_η_h2 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : have X := X t s; X = 1

theorem Elligator.Elligator1.u_η_h1 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : have u := u t; u = 1

theorem Elligator.Elligator1.t_η_h1 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : ↑t = 0

theorem Elligator.Elligator1.v_η_h1 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : have v := v t s; have r := r s; v = r ^ 2

theorem Elligator.Elligator1.Y_η_h1 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : have Y := Y t s q; have c := c s; have r := r s; Y = r * LegendreSymbol.χ c

theorem Elligator.Elligator1.y_η_h1 {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) (η_h1 : have P := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; have r := r s; have η_of_P := η ↑P; η_of_P * r = -2) : have r := r s; have y := y t s; y = (r - 4) / (r + 4)

theorem Elligator.Elligator1.y_of_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) : have y := y ⟨0, ⋯⟩ s; have r := r s; y = (r - 4) / (r + 4)

theorem Elligator.Elligator1.ϕ_of_t_eq_zero_one {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 ϕ := ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod; ↑ϕ = (0, 1)

theorem Elligator.Elligator1.y_add_one_eq_two {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 y := P.2; y + 1 = 2

def Elligator.Elligator1.ϕOverFProp1 {F : Type u_1} [Field F] (P : F × F) : Prop

ϕOverFProp1 is the first property fulfilled by Ps in EOverF. This property does not have to consider a dedicated field F with q. This restriction is defined during the context evolution.

Original: Section "3.3 Inverting the map", Theorem 3

Equations

• Elligator.Elligator1.ϕOverFProp1 P = (P.2 + 1 ≠ 0)

def Elligator.Elligator1.ϕOverFProp2 {F : Type u_1} [Field F] (s : F) (P : F × F) : Prop

ϕOverFProp2 is the second property fulfilled by Ps in EOverF.

Original: Section "3.3 Inverting the map", Theorem 3

Equations

• Elligator.Elligator1.ϕOverFProp2 s P = IsSquare ((1 + Elligator.Elligator1.η P * Elligator.Elligator1.r s) ^ 2 - 1)

def Elligator.Elligator1.ϕOverFProp3 {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (s : F) (P : F × F) : Prop

ϕOverFProp3 is the third property fulfilled by Ps in EOverF.

Original: Section "3.3 Inverting the map", Theorem 3

Equations

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

def Elligator.Elligator1.ϕOverFProps {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (s : F) (P : F × F) : Prop

ϕOverFProps combines the previously defined properties which are fulfilled by Ps in EOverF, i.e. ϕOverFProp1, ϕOverFProp2 and ϕOverFProp3.

Original: Section "3.3 Inverting the map", Theorem 3

Equations

• Elligator.Elligator1.ϕOverFProps s P = (Elligator.Elligator1.ϕOverFProp1 P ∧ Elligator.Elligator1.ϕOverFProp2 s P ∧ Elligator.Elligator1.ϕOverFProp3 s P)

def Elligator.Elligator1.ϕOverF {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) : Set (F × F)

ϕOverF is the set of Ps produced by ϕ.

Original: Section "3.2 The map", Definition 2

Equations

• Elligator.Elligator1.ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod = Set.range fun (t : F) => ↑(Elligator.Elligator1.ϕ t hs_ne_zero sq_ne_pm_two hq_card hq_mod)

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop1_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); ϕOverFProp1 P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop1_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); ϕOverFProp1 P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop1 {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); ϕOverFProp1 P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop2_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); ϕOverFProp2 s P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop2_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); ϕOverFProp2 s P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop2 {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); ϕOverFProp2 s P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop3_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); ϕOverFProp3 s P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop3_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); ϕOverFProp3 s P

theorem Elligator.Elligator1.P_in_ϕOverF_with_prop3 {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; ϕOverFProp3 s ↑P

theorem Elligator.Elligator1.P_props_of_P_in_ϕOverF {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); P ∈ ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod → ϕOverFProps s P

theorem Elligator.Elligator1.P_of_ϕ_in_ϕOverF {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 ϕOverF := ϕOverF hs_ne_zero sq_ne_pm_two hq_card hq_mod; P ∈ ϕOverF

theorem Elligator.Elligator1.P_of_ϕ_fulfills_ϕOverFProps {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); ϕOverFProps s P