noncomputable def c {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) : F

c(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = 2 / s ^ 2

noncomputable def r {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) : F

r(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def d {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) : F

d(s) is a constant defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def u {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : F

u(t) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

• u t q field_cardinality q_prime_power q_mod_4_congruent_3 = (1 - ↑t) / (1 + ↑t)

noncomputable def v {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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) : F

v(t, s) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def X {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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) : F

X(t, s) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def Y {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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) : F

Y(t, s) is a function defined in the paper.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def x {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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) : F

x(t, s) is a function defined in the paper. It is the x-coordinate of the point on the curve.

Paper definition at chapter 3.2 theorem 1.

Equations

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

noncomputable def y {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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) : F

y(t, s) is a function defined in the paper. It is the y-coordinate of the point on the curve.

Paper definition at chapter 3.2 theorem 1.

Equations

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

theorem c_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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ≠ 0

theorem Y_defined {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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ^ 2 ≠ 0

theorem s_pow_two_ne_two {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) : s ^ 2 ≠ 2

theorem s_pow_two_ne_neg_two {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) : s ^ 2 ≠ -2

theorem c_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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ≠ 1

theorem c_ne_neg_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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ≠ -1

theorem c_add_one_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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s + 1 ≠ 0

theorem c_sub_one_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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s - 1 ≠ 0

theorem c_h {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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s * (c_of_s - 1) * (c_of_s + 1) ≠ 0

theorem r_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) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; r_of_s ≠ 0

theorem d_nonsquare {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) : have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ¬IsSquare d_of_s

theorem one_sub_t_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 - ↑t ≠ 0

theorem one_add_t_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 + ↑t ≠ 0

theorem u_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : u t q field_cardinality q_prime_power q_mod_4_congruent_3 ≠ 0

theorem u_pow_two_ne_zero {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; u_of_t ^ 2 ≠ 0

theorem c_pow_two_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) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; c_of_s ^ 2 ≠ 0

theorem v_h1_third_factor_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; u_of_t ^ 2 + 1 / c_of_s ^ 2 ≠ 0

theorem r_h1 {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) : have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; r_of_s ^ 2 - 2 = c_of_s ^ 2 + 1 / c_of_s ^ 2

theorem v_h1 {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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; v_of_t = u_of_t * (u_of_t ^ 2 + c_of_s ^ 2) * (u_of_t ^ 2 + 1 / c_of_s ^ 2)

theorem v_h1_second_factor_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have c_of_s := c s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; u_of_t ^ 2 + c_of_s ^ 2 ≠ 0

theorem v_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v_of_t ≠ 0

theorem u_defined {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 + ↑t ≠ 0

theorem X_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X_of_t ≠ 0

theorem Y_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y_of_t ≠ 0

theorem X_mul_Y_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X_of_t * Y_of_t ≠ 0

theorem x_defined {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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ≠ 0

theorem one_add_X_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; 1 + X_of_t ≠ 0

theorem x_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x_of_t ≠ 0

theorem map_fulfills_specific_equation {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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 r_of_s := r 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 Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y_of_t ^ 2 = X_of_t ^ 5 + (r_of_s ^ 2 - 2) * X_of_t ^ 3 + X_of_t

theorem y_divisor_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have r_of_s := r 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; r_of_s * X_of_t + (1 + X_of_t) ^ 2 ≠ 0

theorem y_defined {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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 * X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 + (1 + X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3) ^ 2 ≠ 0

theorem y_add_one_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) (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; y_of_t + 1 ≠ 0

theorem u_mul_v_mul_X_mul_Y_mul_x_mul_y_add_one_ne_zero {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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 u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3; have v_of_t := v 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 Y_of_t := Y 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 y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; u_of_t * v_of_t * X_of_t * Y_of_t * x_of_t * (y_of_t + 1) ≠ 0

theorem map_fulfills_curve_equation {F : Type u_1} [Field F] [Fintype F] (t : { n : F // n ≠ 1 ∧ n ≠ -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 x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x_of_t ^ 2 + y_of_t ^ 2 = 1 + d_of_s * x_of_t ^ 2 * y_of_t ^ 2

noncomputable def ϕ {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) : F × F

ϕ(t, s) is a function defined in the paper. It maps a numer t in F s to a point on the curve.

Paper definition at chapter 3.2 definition 2.

Equations

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

def E_over_F {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) : Set (F × F)

E_over_F(s, q) is the set of points on the curve defined by the equation in the paper.

Paper definition at chapter 3.3 theorem 3.

Equations

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

noncomputable def ϕ_over_F_prop1 {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : Prop

Equations

• ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 point = (point.2 + 1 ≠ 0)

noncomputable def η {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (point : F × F) : F

η(s, q, point) is a function defined in the paper.

Paper definition at chapter 3.3 theorem 3.

Equations

• η q field_cardinality q_prime_power q_mod_4_congruent_3 point = (point.2 - 1) / (2 * (point.2 + 1))

def ϕ_over_F_prop2 {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 : F × F) : Prop

Equations

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

def ϕ_over_F_prop3 {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 : F × F) : Prop

Equations

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

noncomputable def ϕ_over_F {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) : Set (F × F)

Equations

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

noncomputable def b (q : ℕ) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : ℕ

Equations

• b q q_prime_power q_mod_4_congruent_3 = ⌊Real.logb 2 ↑q⌋.toNat

@[reducible, inline]

abbrev Binary : Type

Equations

• Binary = Fin 2

def S (b : ℕ) : Set (List Binary)

Equations

• S b = {n : List Binary | n.length = b}

noncomputable def σ {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (τ : { n : List Binary // n ∈ S (b q q_prime_power q_mod_4_congruent_3) }) : F

Equations

• σ q field_cardinality q_prime_power q_mod_4_congruent_3 τ = ∑ i ∈ Finset.range (b q q_prime_power q_mod_4_congruent_3 - 1), ↑↑(↑τ)[i]! * 2 ^ i

noncomputable def ι {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) (τ : { n : List Binary // n ∈ S (b q q_prime_power q_mod_4_congruent_3) }) : F × F

`ιis the injective map that maps a binary stringτto a point on the curveE(F_q)`.

Paper definition at chapter 3.4 Theorem 4.

Equations

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

theorem S_cardinality (q : ℕ) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : (S (b q q_prime_power q_mod_4_congruent_3)).ncard = (q + 1) / 2

theorem ι_injective_map {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) (τ₁ τ₂ : { n : List Binary // n ∈ S (b q q_prime_power q_mod_4_congruent_3) }) : ι s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 τ₁ = ι s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 τ₂ → τ₁ = τ₂

noncomputable def ι_S {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) : Set (F × F)

Equations

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

theorem ι_S_eq_ϕ_over_F {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) : have ϕ_over_F_of_s := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ι_S_of_s := ι_S s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_over_F_of_s = ι_S_of_s