theorem u_comparison {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have u2 := u ⟨t2, h2_2⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; u2 = 1 / u1

theorem v_comparison {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have r_of_s := r s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v2 = 1 / u1 ^ 5 + (r_of_s ^ 2 - 2) * 1 / u1 ^ 3 + 1 / u1

theorem v_comparison_implication1 {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v1 := v ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v2 * u1 ^ 6 = v1

theorem v_comparison_implication2 {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v1 := v ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; v2 = v1 / u1 ^ 6

theorem v_comparison_implication3 {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; have t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_u1_pow_6 := LegendreSymbol.χ (u1 ^ 6) q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_u1_pow_6 = 1

theorem v_comparison_implication4 {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have u1 := u ⟨t1, h2_1⟩ q field_cardinality q_prime_power q_mod_4_congruent_3; have v1 := v ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have v2 := v ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_v1 := LegendreSymbol.χ v1 q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_v2 := LegendreSymbol.χ v2 q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_v2 = χ_of_v1

theorem X_comparison {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have X1 := X ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2 := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; X2 = 1 / X1

theorem Y_comparison {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have X1 := X ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have X2 := X ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y1 := Y ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have Y2 := Y ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; Y2 = Y1 / X1 ^ 3

theorem x_comparison {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have x1 := x ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have x2 := x ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; x2 = x1

theorem y_comparison {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) (h2_1 : t ≠ 1 ∧ t ≠ -1) (h2_2 : -t ≠ 1 ∧ -t ≠ -1) : let t1 := t; let t2 := -t1; have y1 := y ⟨t1, h2_1⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have y2 := y ⟨t2, h2_2⟩ s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; y2 = y1

theorem ϕ_of_t_eq_ϕ_of_neg_t_base_case {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 ϕ_of_t := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t

theorem ϕ_of_t_eq_ϕ_of_neg_t_main_case {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 ϕ_of_t := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t

theorem ϕ_of_t_eq_ϕ_of_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 ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t

theorem ϕ_inv_only_two_specific_preimages_mpr {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 ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ¬∃ (w : { n : F // n ≠ t ∧ n ≠ -t }), ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t

theorem ϕ_inv_only_two_specific_preimages {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 ϕ_of_t := ϕ t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_of_neg_t := ϕ (-t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t = ϕ_of_neg_t ↔ ¬∃ (w : { n : F // n ≠ t ∧ n ≠ -t }), ϕ (↑w) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = ϕ_of_t

theorem point_in_ϕ_over_F_with_prop1_base_case {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 point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem point_in_ϕ_over_F_with_prop1_main_case {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 point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem point_in_ϕ_over_F_with_prop1 {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; ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem point_in_ϕ_over_F_with_prop2_base_case {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 point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem y_h1 {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 y_of_t := y 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 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; X_of_t ^ 2 + (2 + r_of_s * (y_of_t - 1) / (y_of_t + 1)) * X_of_t + 1 = 0

theorem point_in_ϕ_over_F_with_prop2_main_case {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 point := ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem point_in_ϕ_over_F_with_prop2 {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; ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point

theorem point_in_E_over_F_with_props_iff_point_in_ϕ_over_F_mp {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 ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 → ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ∧ ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ∧ ϕ_over_F_prop3 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point) → ↑point ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3

theorem point_in_E_over_F_with_props_iff_point_in_ϕ_over_F_mpr {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 → ∀ (h : ↑point ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3), ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ∧ ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ∧ ϕ_over_F_prop3 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point

theorem point_in_E_over_F_with_props_iff_point_in_ϕ_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) (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 ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 → ϕ_over_F_prop1 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ∧ ϕ_over_F_prop2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ∧ ϕ_over_F_prop3 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 ↑point ↔ ↑point ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3

theorem E_over_F_subset_ϕ_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 E_over_F_of_s := E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have ϕ_over_F_q_of_s := ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; E_over_F_of_s ⊆ ϕ_over_F_q_of_s

theorem point_in_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) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have E_over_F_of_s := E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ↑point ∈ E_over_F_of_s

noncomputable def X2 {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (h : ↑point ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3) : F

Equations

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

noncomputable def z {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

Equations

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

noncomputable def u2 {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

Equations

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

noncomputable def t2 {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : F

Equations

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

theorem X2_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) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have y := (↑point).2; 2 * (y + 1) ≠ 0

theorem z_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) : 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 t2_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) (point : { p : F × F // p ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) : have u2_of_point := u2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point; 1 + u2_of_point ≠ 0

theorem invmap_representative_base_case {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (t' : { n : F // n = 1 ∨ n = -1 }) (representative : ↑t' = t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point) : have ϕ_of_t' := ϕ (↑t') s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; ϕ_of_t' = (0, 1)

invmap_representative is ...

Paper definition at chapter 3.3 Theorem 3.3.

theorem invmap_representative_main_case {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 ∈ ϕ_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }) (t' : { n : F // n ≠ 1 ∧ n ≠ -1 }) (representative : ↑t' = t2 s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 point) : have ϕ_of_t' := ϕ (↑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; ϕ_of_t' = (x_of_t', y_of_t')

invmap_representative is ...

Paper definition at chapter 3.3 Theorem 3.3.