theorem Elligator.Elligator1.t2_eq_one {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t = 1 ∨ t = -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have t2_of_point := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; t2_of_point = 1

theorem Elligator.Elligator1.t2_eq_t {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (X_h : have point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_t = X_of_t) : have point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have t2_of_point := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; t2_of_point = ↑t

theorem Elligator.Elligator1.t2_eq_t' {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (X_h : have point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have h2_2 := ⋯; have X'_of_t := X ⟨-↑t, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2_of_t := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X2_of_t = X'_of_t) : have point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have t2_of_point := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have t' := -↑t; t2_of_point = t'

theorem Elligator.Elligator1.t2_in_t_or_neg_t {F : Type u_1} [Field F] [Fintype F] (t s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : have point := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have t' := -t; have t2_of_point := t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; t2_of_point = t ∨ t2_of_point = t'

noncomputable def Elligator.Elligator1.t' {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) : F

Equations

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

theorem Elligator.Elligator1.t'_ne_one_and_t'_ne_neg_one_of_X2_ne_one {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; X ≠ 1 → t ≠ 1 ∧ t ≠ -1

theorem Elligator.Elligator1.one_add_t'_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; X ≠ 1 → t + 1 ≠ 0

theorem Elligator.Elligator1.u'_eq_one_sub_t'_over_one_add_t' {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; have u := u' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; X ≠ 1 → u = (1 - t) / (1 + t)

theorem Elligator.Elligator1.u'_eq_u {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X ≠ 1) : have u' := u' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have u := u ⟨t, t_h⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; u' = u

theorem Elligator.Elligator1.v'_eq_v {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X ≠ 1) : have v' := v' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have v := v ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v' = v

theorem Elligator.Elligator1.X'_eq_X {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X ≠ 1) : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have X := X ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X' = X

theorem Elligator.Elligator1.Y'_eq_Y {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X ≠ 1) : have Y' := Y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have Y := Y ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y' = Y

noncomputable def Elligator.Elligator1.x' {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) : F

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] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X' ≠ 1) : let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have x := x ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have x' := x' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; x' = x

noncomputable def Elligator.Elligator1.y' {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) : F

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] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X' ≠ 1) : let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have y := y ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y' := y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; y' = y

theorem Elligator.Elligator1.x'_and_y'_fulfill_curve_equation {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X' ≠ 1) : have x' := x' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have y' := y' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; let d := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have d_h := ⋯; edwards_curve_equation x' y' ⟨d, d_h⟩ q field_cardinality q_prime_power q_mod_4_congruent_3

theorem Elligator.Elligator1.y_of_t_eq_y_of_point {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X' ≠ 1) : let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have y_of_t := y ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y_of_point := (↑point).2; y_of_t = y_of_point

theorem Elligator.Elligator1.x_of_t_eq_x_of_point {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X' ≠ 1) : let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have x_of_t := x ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have x_of_point := (↑point).1; x_of_t = x_of_point

theorem Elligator.Elligator1.x_y_of_point_eq_x_y_of_t {F : Type u_1} [Field F] [Fintype F] (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : { p : F × F // p ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (point_props : ϕ_over_F_props s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) (x_ne_zero : (↑point).1 ≠ 0) (y_ne_one : (↑point).2 ≠ 1) (X_h : have X' := X2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point; X' ≠ 1) : let t := t' s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point point_props; have t_h := ⋯; have y_of_t := y ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y_of_point := (↑point).2; have x_of_t := x ⟨t, t_h⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have x_of_point := (↑point).1; (x_of_t, y_of_t) = (x_of_point, y_of_point)