import Mathlib import Definitions.Def_TateCurve_XMultAlignment import Theorems.Thm_TateCurve_pointY_inv import Theorems.Thm_TateCurve_pointY_zpow_mul import Theorems.Thm_TateCurve_pointX_qExpansion set_option autoImplicit false set_option linter.unusedSectionVars false namespace WeierstrassCurve section Bezout variable {F : Type*} [Field F] (W : WeierstrassCurve F) def bezF (x : F) : F := (8 * W.b₂ ^ 3 * W.b₆ - 8 * W.b₂ ^ 2 * W.b₄ ^ 2 + 16 * W.b₂ ^ 2 * W.b₈ - 336 * W.b₂ * W.b₄ * W.b₆ + 288 * W.b₄ ^ 3 - 384 * W.b₄ * W.b₈ + 1296 * W.b₆ ^ 2) * x ^ 2 + (2 * W.b₂ ^ 4 * W.b₆ - 2 * W.b₂ ^ 3 * W.b₄ ^ 2 - 80 * W.b₂ ^ 2 * W.b₄ * W.b₆ + 72 * W.b₂ * W.b₄ ^ 3 + 32 * W.b₂ * W.b₄ * W.b₈ + 360 * W.b₂ * W.b₆ ^ 2 - 144 * W.b₄ ^ 2 * W.b₆ - 576 * W.b₆ * W.b₈) * x + (-W.b₂ ^ 4 * W.b₈ + 5 * W.b₂ ^ 3 * W.b₄ * W.b₆ - 4 * W.b₂ ^ 2 * W.b₄ ^ 3 + 48 * W.b₂ ^ 2 * W.b₄ * W.b₈ + W.b₂ ^ 2 * W.b₆ ^ 2 - 204 * W.b₂ * W.b₄ ^ 2 * W.b₆ - 176 * W.b₂ * W.b₆ * W.b₈ + 144 * W.b₄ ^ 4 - 384 * W.b₄ ^ 2 * W.b₈ + 864 * W.b₄ * W.b₆ ^ 2 + 256 * W.b₈ ^ 2) def bezG (x : F) : F := (-2 * W.b₂ ^ 3 * W.b₆ + 2 * W.b₂ ^ 2 * W.b₄ ^ 2 - 4 * W.b₂ ^ 2 * W.b₈ + 84 * W.b₂ * W.b₄ * W.b₆ - 72 * W.b₄ ^ 3 + 96 * W.b₄ * W.b₈ - 324 * W.b₆ ^ 2) * x ^ 3 + (W.b₂ ^ 3 * W.b₈ - W.b₂ ^ 2 * W.b₄ * W.b₆ - 32 * W.b₂ * W.b₄ * W.b₈ - 9 * W.b₂ * W.b₆ ^ 2 + 36 * W.b₄ ^ 2 * W.b₆ + 144 * W.b₆ * W.b₈) * x ^ 2 + (2 * W.b₂ ^ 3 * W.b₄ * W.b₆ - 2 * W.b₂ ^ 2 * W.b₄ ^ 3 + 2 * W.b₂ ^ 2 * W.b₄ * W.b₈ + 2 * W.b₂ ^ 2 * W.b₆ ^ 2 - 84 * W.b₂ * W.b₄ ^ 2 * W.b₆ + 8 * W.b₂ * W.b₆ * W.b₈ + 72 * W.b₄ ^ 4 - 48 * W.b₄ ^ 2 * W.b₈ + 270 * W.b₄ * W.b₆ ^ 2 - 64 * W.b₈ ^ 2) * x + (-W.b₂ ^ 3 * W.b₄ * W.b₈ + 4 * W.b₂ ^ 3 * W.b₆ ^ 2 - 3 * W.b₂ ^ 2 * W.b₄ ^ 2 * W.b₆ + 7 * W.b₂ ^ 2 * W.b₆ * W.b₈ + 36 * W.b₂ * W.b₄ ^ 2 * W.b₈ - 162 * W.b₂ * W.b₄ * W.b₆ ^ 2 + 16 * W.b₂ * W.b₈ ^ 2 + 108 * W.b₄ ^ 3 * W.b₆ - 432 * W.b₄ * W.b₆ * W.b₈ + 729 * W.b₆ ^ 3) theorem bezout_Φ_two_Ψ₂Sq (x : F) : W.bezF x * (W.Φ 2).eval x + W.bezG x * W.Ψ₂Sq.eval x = W.Δ ^ 2 := by rw [bezF, bezG, Affine.eval_Φ_two (W := W), Affine.eval_Ψ₂Sq (W := W)] simp only [Δ] linear_combination (-12 * W.b₂ ^ 2 * W.b₄ * W.b₈ - 4 * W.b₂ ^ 2 * W.b₆ ^ 2 + 80 * W.b₂ * W.b₄ ^ 2 * W.b₆ + 32 * W.b₂ * W.b₆ * W.b₈ - 64 * W.b₄ ^ 4 + 112 * W.b₄ ^ 2 * W.b₈ - 324 * W.b₄ * W.b₆ ^ 2 - 64 * W.b₈ ^ 2) * W.b_relation theorem Δ_sq_eq_zero_of_eval_eq_zero {x : F} (hΦ : (W.Φ 2).eval x = 0) (hΨ : W.Ψ₂Sq.eval x = 0) : W.Δ ^ 2 = 0 := by rw [← W.bezout_Φ_two_Ψ₂Sq x, hΦ, hΨ, mul_zero, mul_zero, add_zero] theorem not_eval_Φ_two_eq_zero [W.IsElliptic] {x : F} (hΨ : W.Ψ₂Sq.eval x = 0) : (W.Φ 2).eval x ≠ 0 := fun hΦ => pow_ne_zero 2 W.isUnit_Δ.ne_zero <| W.Δ_sq_eq_zero_of_eval_eq_zero hΦ hΨ end Bezout end WeierstrassCurve namespace TateCurve section AnnulusTranslateExtra variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {q u : K} theorem exists_zpow_mul_norm_Ioc (hq0 : q ≠ 0) (hq : ‖q‖ < 1) (hu0 : u ≠ 0) : ∃ n : ℤ, ‖q‖ < ‖q ^ n * u‖ ∧ ‖q ^ n * u‖ ≤ 1 := by have hq_pos : (0 : ℝ) < ‖q‖ := norm_pos_iff.mpr hq0 have hu_pos : (0 : ℝ) < ‖u‖ := norm_pos_iff.mpr hu0 have hq_ne : (‖q‖ : ℝ) ≠ 0 := ne_of_gt hq_pos have hy : (1 : ℝ) < ‖q‖⁻¹ := one_lt_inv_iff₀.mpr ⟨hq_pos, hq⟩ obtain ⟨n, hn1, hn2⟩ := exists_mem_Ioc_zpow hu_pos hy have hqk_pos : (0 : ℝ) < ‖q‖ ^ (n + 1 : ℤ) := zpow_pos hq_pos _ have hcancel : ∀ m : ℤ, ‖q‖⁻¹ ^ m * ‖q‖ ^ m = 1 := fun m => by rw [← mul_zpow, inv_mul_cancel₀ hq_ne, one_zpow] refine ⟨n + 1, ?_, ?_⟩ · have hkey : ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ n = ‖q‖ := by rw [zpow_add₀ hq_ne, zpow_one] calc ‖q‖ ^ n * ‖q‖ * ‖q‖⁻¹ ^ n = ‖q‖⁻¹ ^ n * (‖q‖ ^ n * ‖q‖) := mul_comm _ _ _ = ‖q‖⁻¹ ^ n * ‖q‖ ^ n * ‖q‖ := (mul_assoc _ _ _).symm _ = 1 * ‖q‖ := by rw [hcancel n] _ = ‖q‖ := one_mul _ have hlt : ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ n < ‖q‖ ^ (n + 1 : ℤ) * ‖u‖ := mul_lt_mul_of_pos_left hn1 hqk_pos rw [norm_mul, norm_zpow] calc ‖q‖ = ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ n := hkey.symm _ < ‖q‖ ^ (n + 1 : ℤ) * ‖u‖ := hlt · have hkey : ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ (n + 1) = 1 := by calc ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ (n + 1) = ‖q‖⁻¹ ^ (n + 1) * ‖q‖ ^ (n + 1) := mul_comm _ _ _ = 1 := hcancel (n + 1) have hle : ‖q‖ ^ (n + 1 : ℤ) * ‖u‖ ≤ ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ (n + 1) := mul_le_mul_of_nonneg_left hn2 hqk_pos.le rw [norm_mul, norm_zpow] calc ‖q‖ ^ (n + 1 : ℤ) * ‖u‖ ≤ ‖q‖ ^ (n + 1 : ℤ) * ‖q‖⁻¹ ^ (n + 1) := hle _ = 1 := hkey end AnnulusTranslateExtra end TateCurve set_option linter.unusedSectionVars false open WeierstrassCurve.Affine open Polynomial open IsUltrametricDist namespace TateCurve variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [CharZero K] [DecidableEq K] variable {q u v : K} section Factorization noncomputable def xPairNum (u v : K) (d : ℕ) : K := (d : K) * (∑ k ∈ Finset.range d, u ^ k * v ^ (d - 1 - k)) * (∑ j ∈ Finset.range d, (u * v) ^ j) noncomputable def xPairCoeff (u v : K) (M : ℕ) : K := (∑ d ∈ M.divisors, xPairNum u v d * (u * v) ^ (M - d)) / (u * v) ^ M lemma xfun_sub_xfun (hu1 : u ≠ 1) (hv1 : v ≠ 1) : xfun u - xfun v = (u - v) * (1 - u * v) * ((1 - u) ^ 2 * (1 - v) ^ 2)⁻¹ := by have h1u : (1 : K) - u ≠ 0 := sub_ne_zero.mpr (Ne.symm hu1) have h1v : (1 : K) - v ≠ 0 := sub_ne_zero.mpr (Ne.symm hv1) rw [xfun, xfun] field_simp ring lemma xDivTerm_sub_mul (hu0 : u ≠ 0) (hv0 : v ≠ 0) (d : ℕ) : (xDivTerm u d - xDivTerm v d) * (u * v) ^ d = -((u - v) * (1 - u * v)) * xPairNum u v d := by have hu' : u⁻¹ ^ d * (u * v) ^ d = v ^ d := by rw [← mul_pow, ← mul_assoc, inv_mul_cancel₀ hu0, one_mul] have hv' : v⁻¹ ^ d * (u * v) ^ d = u ^ d := by rw [← mul_pow, mul_comm u v, ← mul_assoc, inv_mul_cancel₀ hv0, one_mul] have hS : (∑ k ∈ Finset.range d, u ^ k * v ^ (d - 1 - k)) * (u - v) = u ^ d - v ^ d := geom_sum₂_mul u v d have hT : (∑ j ∈ Finset.range d, (u * v) ^ j) * (u * v - 1) = (u * v) ^ d - 1 := geom_sum_mul (u * v) d have step1 : (xDivTerm u d - xDivTerm v d) * (u * v) ^ d = (d : K) * ((u ^ d - v ^ d) * ((u * v) ^ d - 1)) := by rw [xDivTerm, xDivTerm] linear_combination ((d : K)) * hu' - (d : K) * hv' rw [step1, xPairNum, ← hS, ← hT] ring lemma xCoeff_sub_xCoeff (hu0 : u ≠ 0) (hv0 : v ≠ 0) {M : ℕ} (hM : M ≠ 0) : xCoeff u M - xCoeff v M = -((u - v) * (1 - u * v)) * xPairCoeff u v M := by have hB : ((u * v) ^ M : K) ≠ 0 := pow_ne_zero M (mul_ne_zero hu0 hv0) rw [xPairCoeff, ← mul_div_assoc, eq_div_iff hB, xCoeff, xCoeff, ← Finset.sum_sub_distrib, Finset.sum_mul, Finset.mul_sum] refine Finset.sum_congr rfl fun d hd => ?_ have hdM : d ≤ M := Nat.le_of_dvd (Nat.pos_of_ne_zero hM) (Nat.mem_divisors.mp hd).1 have hsplit : (u * v) ^ M = (u * v) ^ d * (u * v) ^ (M - d) := by rw [← pow_add] congr 1 omega rw [hsplit, ← mul_assoc, xDivTerm_sub_mul hu0 hv0 d, mul_assoc] lemma norm_xPairNum_le (hu1 : ‖u‖ ≤ 1) (hv1 : ‖v‖ ≤ 1) (d : ℕ) : ‖xPairNum u v d‖ ≤ 1 := by have huv1 : ‖u * v‖ ≤ 1 := by rw [norm_mul] exact mul_le_one₀ hu1 (norm_nonneg v) hv1 have hS : ‖∑ k ∈ Finset.range d, u ^ k * v ^ (d - 1 - k)‖ ≤ 1 := by refine norm_sum_le_of_forall_le_of_nonneg zero_le_one fun k _ => ?_ rw [norm_mul, norm_pow, norm_pow] exact mul_le_one₀ (pow_le_one₀ (norm_nonneg u) hu1) (pow_nonneg (norm_nonneg v) _) (pow_le_one₀ (norm_nonneg v) hv1) have hT : ‖∑ j ∈ Finset.range d, (u * v) ^ j‖ ≤ 1 := by refine norm_sum_le_of_forall_le_of_nonneg zero_le_one fun j _ => ?_ rw [norm_pow] exact pow_le_one₀ (norm_nonneg _) huv1 calc ‖xPairNum u v d‖ = ‖(d : K)‖ * ‖∑ k ∈ Finset.range d, u ^ k * v ^ (d - 1 - k)‖ * ‖∑ j ∈ Finset.range d, (u * v) ^ j‖ := by rw [xPairNum, norm_mul, norm_mul] _ ≤ 1 * 1 * 1 := mul_le_mul (mul_le_mul (norm_natCast_le_one K d) hS (norm_nonneg _) zero_le_one) hT (norm_nonneg _) (by norm_num) _ = 1 := by norm_num lemma norm_xPairCoeff_le (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu1 : ‖u‖ ≤ 1) (hv1 : ‖v‖ ≤ 1) (M : ℕ) : ‖xPairCoeff u v M‖ ≤ (‖u * v‖⁻¹) ^ M := by have huv0 : ‖u * v‖ ≠ 0 := norm_ne_zero_iff.mpr (mul_ne_zero hu0 hv0) have huv1 : ‖u * v‖ ≤ 1 := by rw [norm_mul] exact mul_le_one₀ hu1 (norm_nonneg v) hv1 have hpos : (0 : ℝ) < ‖u * v‖ ^ M := pow_pos (lt_of_le_of_ne (norm_nonneg _) (Ne.symm huv0)) M have hA : ‖∑ d ∈ M.divisors, xPairNum u v d * (u * v) ^ (M - d)‖ ≤ 1 := by refine norm_sum_le_of_forall_le_of_nonneg zero_le_one fun d _ => ?_ rw [norm_mul, norm_pow] exact mul_le_one₀ (norm_xPairNum_le hu1 hv1 d) (pow_nonneg (norm_nonneg _) _) (pow_le_one₀ (norm_nonneg _) huv1) rw [xPairCoeff, norm_div, norm_pow, div_le_iff₀ hpos, inv_pow, inv_mul_cancel₀ (ne_of_gt hpos)] exact hA lemma summable_xCoeff_mul_pow (hq : ‖q‖₊ < 1) (hqu : ‖q * u‖₊ < 1) (hqu' : ‖q * u⁻¹‖₊ < 1) : Summable (fun N : ℕ => xCoeff u (N + 1) * q ^ (N + 1)) := by have hC1 : (1 : ℝ) ≤ growthBound u := one_le_growthBound u have hr : ‖q‖ * growthBound u < 1 := norm_mul_growthBound_lt_one hq hqu hqu' have hr0 : (0 : ℝ) ≤ ‖q‖ * growthBound u := mul_nonneg (norm_nonneg q) (zero_le_one.trans hC1) refine Summable.of_norm ?_ refine Summable.of_nonneg_of_le (fun N => norm_nonneg _) (fun N => ?_) ((summable_geometric_of_lt_one hr0 hr).mul_left (‖q‖ * growthBound u)) rw [norm_mul, norm_pow] have h1 : ‖xCoeff u (N + 1)‖ ≤ growthBound u ^ (N + 1) := by refine norm_sum_le_of_forall_le_of_nonneg (pow_nonneg (zero_le_one.trans hC1) _) fun d hd => ?_ have hdM : d ≤ N + 1 := Nat.le_of_dvd (Nat.succ_pos N) (Nat.mem_divisors.mp hd).1 exact (norm_xDivTerm_le u d).trans (pow_le_pow_right₀ hC1 hdM) calc ‖xCoeff u (N + 1)‖ * ‖q‖ ^ (N + 1) ≤ growthBound u ^ (N + 1) * ‖q‖ ^ (N + 1) := mul_le_mul_of_nonneg_right h1 (pow_nonneg (norm_nonneg q) _) _ = (‖q‖ * growthBound u) ^ (N + 1) := by rw [← mul_pow]; ring_nf _ = (‖q‖ * growthBound u) * (‖q‖ * growthBound u) ^ N := by rw [pow_succ]; ring lemma norm_tsum_xPairCoeff_le (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu1 : ‖u‖ ≤ 1) (hv1 : ‖v‖ ≤ 1) (huv : ‖q‖ < ‖u * v‖) : ‖∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)‖ ≤ ‖q‖ / ‖u * v‖ := by have huvpos : (0 : ℝ) < ‖u * v‖ := norm_pos_iff.mpr (mul_ne_zero hu0 hv0) have hr0 : (0 : ℝ) ≤ ‖q‖ / ‖u * v‖ := div_nonneg (norm_nonneg q) (norm_nonneg _) have hr1 : ‖q‖ / ‖u * v‖ ≤ 1 := le_of_lt ((div_lt_one huvpos).mpr huv) refine norm_tsum_le_of_forall_le_of_nonneg hr0 fun N => ?_ rw [norm_mul, norm_pow] calc ‖xPairCoeff u v (N + 1)‖ * ‖q‖ ^ (N + 1) ≤ (‖u * v‖⁻¹) ^ (N + 1) * ‖q‖ ^ (N + 1) := mul_le_mul_of_nonneg_right (norm_xPairCoeff_le hu0 hv0 hu1 hv1 (N + 1)) (pow_nonneg (norm_nonneg q) _) _ = (‖q‖ / ‖u * v‖) ^ (N + 1) := by rw [← mul_pow] congr 1 rw [div_eq_mul_inv, mul_comm] _ ≤ ‖q‖ / ‖u * v‖ := pow_le_of_le_one hr0 hr1 (Nat.succ_ne_zero N) theorem pointX_sub_pointX_factor (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu : OffLattice q u) (hv : OffLattice q v) (hu1 : ‖u‖ ≤ 1) (hv1 : ‖v‖ ≤ 1) (huv : ‖q‖ < ‖u * v‖) : pointX q u - pointX q v = (u - v) * (1 - u * v) * (((1 - u) ^ 2 * (1 - v) ^ 2)⁻¹ - ∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)) := by have hqR : ‖q‖ < 1 := by exact_mod_cast hq have hunorm : ‖q‖ < ‖u‖ := lt_of_lt_of_le huv (by rw [norm_mul] exact mul_le_of_le_one_right (norm_nonneg u) hv1) have hvnorm : ‖q‖ < ‖v‖ := lt_of_lt_of_le huv (by rw [norm_mul, mul_comm] exact mul_le_of_le_one_right (norm_nonneg v) hu1) have hqu : ‖q * u‖₊ < 1 := by have h : ‖q * u‖ < 1 := lt_of_le_of_lt (by rw [norm_mul]; exact mul_le_of_le_one_right (norm_nonneg q) hu1) hqR exact_mod_cast h have hqu' : ‖q * u⁻¹‖₊ < 1 := by have hupos : (0 : ℝ) < ‖u‖ := norm_pos_iff.mpr hu0 have h : ‖q * u⁻¹‖ < 1 := by rw [norm_mul, norm_inv, ← div_eq_mul_inv, div_lt_one hupos] exact hunorm exact_mod_cast h have hqv : ‖q * v‖₊ < 1 := by have h : ‖q * v‖ < 1 := lt_of_le_of_lt (by rw [norm_mul]; exact mul_le_of_le_one_right (norm_nonneg q) hv1) hqR exact_mod_cast h have hqv' : ‖q * v⁻¹‖₊ < 1 := by have hvpos : (0 : ℝ) < ‖v‖ := norm_pos_iff.mpr hv0 have h : ‖q * v⁻¹‖ < 1 := by rw [norm_mul, norm_inv, ← div_eq_mul_inv, div_lt_one hvpos] exact hvnorm exact_mod_cast h have hu1' : u ≠ 1 := by have := hu 0 rwa [zpow_zero, one_mul] at this have hv1' : v ≠ 1 := by have := hv 0 rwa [zpow_zero, one_mul] at this have hsum_u : Summable (fun N : ℕ => xCoeff u (N + 1) * q ^ (N + 1)) := summable_xCoeff_mul_pow hq hqu hqu' have hsum_v : Summable (fun N : ℕ => xCoeff v (N + 1) * q ^ (N + 1)) := summable_xCoeff_mul_pow hq hqv hqv' have hxfun : xfun u - xfun v = (u - v) * (1 - u * v) * ((1 - u) ^ 2 * (1 - v) ^ 2)⁻¹ := xfun_sub_xfun hu1' hv1' have htails : (∑' N : ℕ, xCoeff u (N + 1) * q ^ (N + 1)) - (∑' N : ℕ, xCoeff v (N + 1) * q ^ (N + 1)) = -((u - v) * (1 - u * v)) * ∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1) := by rw [← Summable.tsum_sub hsum_u hsum_v, ← tsum_mul_left] refine tsum_congr fun N => ?_ rw [← sub_mul, xCoeff_sub_xCoeff hu0 hv0 (Nat.succ_ne_zero N), mul_assoc] rw [pointX_qExpansion hq0 hq hu0 hu hqu hqu', pointX_qExpansion hq0 hq hv0 hv hqv hqv'] calc (xfun u + ∑' N : ℕ, xCoeff u (N + 1) * q ^ (N + 1)) - (xfun v + ∑' N : ℕ, xCoeff v (N + 1) * q ^ (N + 1)) = (xfun u - xfun v) + ((∑' N : ℕ, xCoeff u (N + 1) * q ^ (N + 1)) - (∑' N : ℕ, xCoeff v (N + 1) * q ^ (N + 1))) := by ring _ = (u - v) * (1 - u * v) * ((1 - u) ^ 2 * (1 - v) ^ 2)⁻¹ + (-((u - v) * (1 - u * v)) * ∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)) := by rw [hxfun, htails] _ = (u - v) * (1 - u * v) * (((1 - u) ^ 2 * (1 - v) ^ 2)⁻¹ - ∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)) := by ring theorem eq_or_mul_eq_one_of_pointX_eq (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu : OffLattice q u) (hv : OffLattice q v) (hu1 : ‖u‖ ≤ 1) (hv1 : ‖v‖ ≤ 1) (huv : ‖q‖ < ‖u * v‖) (hX : pointX q u = pointX q v) : u = v ∨ u * v = 1 := by have hu1' : u ≠ 1 := by have := hu 0 rwa [zpow_zero, one_mul] at this have hv1' : v ≠ 1 := by have := hv 0 rwa [zpow_zero, one_mul] at this have h1u : (1 : K) - u ≠ 0 := sub_ne_zero.mpr (Ne.symm hu1') have h1v : (1 : K) - v ≠ 0 := sub_ne_zero.mpr (Ne.symm hv1') have hG : ((1 - u) ^ 2 * (1 - v) ^ 2)⁻¹ - (∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)) ≠ 0 := by intro h0 have hmain_ne : ((1 - u) ^ 2 * (1 - v) ^ 2 : K) ≠ 0 := mul_ne_zero (pow_ne_zero 2 h1u) (pow_ne_zero 2 h1v) have h1u_le : ‖(1 : K) - u‖ ≤ 1 := by have h := nnnorm_add_le_max (1 : K) (-u) rw [nnnorm_neg, nnnorm_one, ← sub_eq_add_neg] at h have hu1'' : ‖u‖₊ ≤ 1 := by exact_mod_cast hu1 have h2 : ‖(1 : K) - u‖₊ ≤ 1 := h.trans (max_le le_rfl hu1'') exact_mod_cast h2 have h1v_le : ‖(1 : K) - v‖ ≤ 1 := by have h := nnnorm_add_le_max (1 : K) (-v) rw [nnnorm_neg, nnnorm_one, ← sub_eq_add_neg] at h have hv1'' : ‖v‖₊ ≤ 1 := by exact_mod_cast hv1 have h2 : ‖(1 : K) - v‖₊ ≤ 1 := h.trans (max_le le_rfl hv1'') exact_mod_cast h2 have hle : ‖((1 - u) ^ 2 * (1 - v) ^ 2 : K)‖ ≤ 1 := by rw [norm_mul, norm_pow, norm_pow] exact mul_le_one₀ (pow_le_one₀ (norm_nonneg _) h1u_le) (pow_nonneg (norm_nonneg _) _) (pow_le_one₀ (norm_nonneg _) h1v_le) have htail : ‖∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)‖ ≤ ‖q‖ / ‖u * v‖ := norm_tsum_xPairCoeff_le hu0 hv0 hu1 hv1 huv have hlt : ‖q‖ / ‖u * v‖ < 1 := (div_lt_one (norm_pos_iff.mpr (mul_ne_zero hu0 hv0))).mpr huv have heq : (((1 - u) ^ 2 * (1 - v) ^ 2 : K))⁻¹ = ∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1) := sub_eq_zero.mp h0 have hone : (1 : K) = ((1 - u) ^ 2 * (1 - v) ^ 2) * ∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1) := by rw [← heq, mul_inv_cancel₀ hmain_ne] have hnorm1 : (1 : ℝ) = ‖((1 - u) ^ 2 * (1 - v) ^ 2 : K)‖ * ‖∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1)‖ := by rw [← norm_mul, ← hone, norm_one] nlinarith [norm_nonneg ((1 - u) ^ 2 * (1 - v) ^ 2 : K), norm_nonneg (∑' N : ℕ, xPairCoeff u v (N + 1) * q ^ (N + 1))] have hfact := pointX_sub_pointX_factor hq0 hq hu0 hv0 hu hv hu1 hv1 huv rw [hX, sub_self] at hfact have h0 : (u - v) * (1 - u * v) = 0 := by rcases mul_eq_zero.mp hfact.symm with h | h · exact h · exact absurd h hG rcases mul_eq_zero.mp h0 with h | h · exact Or.inl (sub_eq_zero.mp h) · exact Or.inr (sub_eq_zero.mp h).symm end Factorization section Fiber private lemma pointX_q_mul_inv (hq0 : q ≠ 0) (hu0 : u ≠ 0) (hu : OffLattice q u) : pointX q (q * u⁻¹) = pointX q u := by have h1 : q * u⁻¹ = q ^ (1 : ℤ) * u⁻¹ := by rw [zpow_one] rw [h1, pointX_zpow_mul hq0, pointX_inv hq0 hu0 hu] theorem exists_zpow_of_pointX_eq_of_pow_lattice (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu : OffLattice q u) (hv : OffLattice q v) {p : ℕ} (hodd : Odd p) {su sv : ℤ} (hpu : u ^ p = q ^ su) (hpv : v ^ p = q ^ sv) (hX : pointX q u = pointX q v) : (∃ k : ℤ, v = q ^ k * u) ∨ (∃ k : ℤ, u * v = q ^ k) := by have hqR : ‖q‖ < 1 := by exact_mod_cast hq have hqpos : (0 : ℝ) < ‖q‖ := norm_pos_iff.mpr hq0 obtain ⟨a, ha1, ha2⟩ := exists_zpow_mul_norm_Ioc hq0 hqR hu0 obtain ⟨b, hb1, hb2⟩ := exists_zpow_mul_norm_Ioc hq0 hqR hv0 set u₀ : K := q ^ a * u with hu₀def set v₀ : K := q ^ b * v with hv₀def have hu₀0 : u₀ ≠ 0 := mul_ne_zero (zpow_ne_zero a hq0) hu0 have hv₀0 : v₀ ≠ 0 := mul_ne_zero (zpow_ne_zero b hq0) hv0 have hu₀off : OffLattice q u₀ := hu.zpow_mul hq0 a have hv₀off : OffLattice q v₀ := hv.zpow_mul hq0 b have hXu₀ : pointX q u₀ = pointX q u := pointX_zpow_mul hq0 a have hXv₀ : pointX q v₀ = pointX q v := pointX_zpow_mul hq0 b have hX₀ : pointX q u₀ = pointX q v₀ := by rw [hXu₀, hXv₀]; exact hX set u₁ : K := q * u₀⁻¹ with hu₁def set v₁ : K := q * v₀⁻¹ with hv₁def have hu₁0 : u₁ ≠ 0 := mul_ne_zero hq0 (inv_ne_zero hu₀0) have hv₁0 : v₁ ≠ 0 := mul_ne_zero hq0 (inv_ne_zero hv₀0) have hu₁off : OffLattice q u₁ := (hu₀off.inv hq0).q_mul hq0 have hv₁off : OffLattice q v₁ := (hv₀off.inv hq0).q_mul hq0 have hXu₁ : pointX q u₁ = pointX q u₀ := pointX_q_mul_inv hq0 hu₀0 hu₀off have hXv₁ : pointX q v₁ = pointX q v₀ := pointX_q_mul_inv hq0 hv₀0 hv₀off have hu₀pos : (0 : ℝ) < ‖u₀‖ := norm_pos_iff.mpr hu₀0 have hv₀pos : (0 : ℝ) < ‖v₀‖ := norm_pos_iff.mpr hv₀0 have hu₁norm : ‖u₁‖ = ‖q‖ / ‖u₀‖ := by rw [hu₁def, norm_mul, norm_inv, div_eq_mul_inv] have hv₁norm : ‖v₁‖ = ‖q‖ / ‖v₀‖ := by rw [hv₁def, norm_mul, norm_inv, div_eq_mul_inv] have hu₁le : ‖u₁‖ ≤ 1 := by rw [hu₁norm] exact le_of_lt ((div_lt_one hu₀pos).mpr ha1) have hv₁le : ‖v₁‖ ≤ 1 := by rw [hv₁norm] exact le_of_lt ((div_lt_one hv₀pos).mpr hb1) have transfer_eq : ∀ k l : ℤ, q ^ k * u = q ^ l * v → ∃ m : ℤ, v = q ^ m * u := by intro k l hkl refine ⟨k - l, ?_⟩ have h1 : v = q ^ (-l) * (q ^ k * u) := by rw [hkl, ← mul_assoc, ← zpow_add₀ hq0, neg_add_cancel, zpow_zero, one_mul] rw [h1, ← mul_assoc, ← zpow_add₀ hq0, show -l + k = k - l by ring] have transfer_mul : ∀ k l m : ℤ, (q ^ k * u) * (q ^ l * v) = q ^ m → ∃ n : ℤ, u * v = q ^ n := by intro k l m hklm refine ⟨m - (k + l), ?_⟩ have h1 : q ^ (k + l) * (u * v) = q ^ m := by rw [zpow_add₀ hq0, ← hklm] ring have h2 : u * v = q ^ (-(k + l)) * q ^ m := by rw [← h1, ← mul_assoc, ← zpow_add₀ hq0, neg_add_cancel, zpow_zero, one_mul] rw [h2, ← zpow_add₀ hq0, show -(k + l) + m = m - (k + l) by ring] by_cases hP1 : ‖q‖ < ‖u₀ * v₀‖ · rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hu₀0 hv₀0 hu₀off hv₀off ha2 hb2 hP1 hX₀ with h | h · refine Or.inl (transfer_eq a b ?_) rw [← hu₀def, ← hv₀def] exact h · refine Or.inr (transfer_mul a b 0 ?_) rw [← hu₀def, ← hv₀def, h, zpow_zero] by_cases hP4 : ‖q‖ < ‖u₁ * v₁‖ · have hX₁ : pointX q u₁ = pointX q v₁ := by rw [hXu₁, hXv₁]; exact hX₀ rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hu₁0 hv₁0 hu₁off hv₁off hu₁le hv₁le hP4 hX₁ with h | h · refine Or.inl (transfer_eq a b ?_) have h0 : u₀ = v₀ := inv_injective (mul_left_cancel₀ hq0 h) rw [← hu₀def, ← hv₀def] exact h0 · refine Or.inr (transfer_mul a b 2 ?_) have hexp : u₀ * v₀ = q ^ (2 : ℤ) := by have h1 := congrArg (fun x => x * (u₀ * v₀)) h simp only [one_mul] at h1 rw [show u₁ * v₁ * (u₀ * v₀) = (q * q) * ((u₀⁻¹ * u₀) * (v₀⁻¹ * v₀)) by rw [hu₁def, hv₁def]; ring] at h1 rw [inv_mul_cancel₀ hu₀0, inv_mul_cancel₀ hv₀0, mul_one, mul_one] at h1 rw [← h1, show (2 : ℤ) = 1 + 1 by norm_num, zpow_add₀ hq0, zpow_one] rw [← hu₀def, ← hv₀def] exact hexp by_cases hP2 : ‖q‖ < ‖u₀ * v₁‖ · have hX₂ : pointX q u₀ = pointX q v₁ := by rw [hXv₁]; exact hX₀ rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hu₀0 hv₁0 hu₀off hv₁off ha2 hv₁le hP2 hX₂ with h | h · refine Or.inr (transfer_mul a b 1 ?_) have hexp : u₀ * v₀ = q := by rw [h, hv₁def, mul_assoc, inv_mul_cancel₀ hv₀0, mul_one] rw [← hu₀def, ← hv₀def, hexp, zpow_one] · refine Or.inl (transfer_eq (a + 1) b ?_) have hexp : v₀ = q * u₀ := by have h1 := congrArg (fun x => x * v₀) h simp only [one_mul] at h1 rw [show u₀ * v₁ * v₀ = (q * u₀) * (v₀⁻¹ * v₀) by rw [hv₁def]; ring] at h1 rw [inv_mul_cancel₀ hv₀0, mul_one] at h1 exact h1.symm have hqq : q * q ^ a = q ^ (a + 1) := by rw [add_comm a 1, zpow_add₀ hq0, zpow_one] have h0 : q ^ b * v = q ^ (a + 1) * u := by rw [← hv₀def, hexp, hu₀def, ← mul_assoc, hqq] exact h0.symm by_cases hP3 : ‖q‖ < ‖u₁ * v₀‖ · have hX₃ : pointX q u₁ = pointX q v₀ := by rw [hXu₁]; exact hX₀ rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hu₁0 hv₀0 hu₁off hv₀off hu₁le hb2 hP3 hX₃ with h | h · refine Or.inr (transfer_mul a b 1 ?_) have hexp : u₀ * v₀ = q := by rw [← h, hu₁def, show u₀ * (q * u₀⁻¹) = q * (u₀ * u₀⁻¹) by ring, mul_inv_cancel₀ hu₀0, mul_one] rw [← hu₀def, ← hv₀def, hexp, zpow_one] · refine Or.inl (transfer_eq a (b + 1) ?_) have hexp : u₀ = q * v₀ := by have h1 := congrArg (fun x => x * u₀) h simp only [one_mul] at h1 rw [show u₁ * v₀ * u₀ = (q * v₀) * (u₀⁻¹ * u₀) by rw [hu₁def]; ring] at h1 rw [inv_mul_cancel₀ hu₀0, mul_one] at h1 exact h1.symm have hqq : q * q ^ b = q ^ (b + 1) := by rw [add_comm b 1, zpow_add₀ hq0, zpow_one] have h0 : q ^ a * u = q ^ (b + 1) * v := by rw [← hu₀def, hexp, hv₀def, ← mul_assoc, hqq] exact h0 · exfalso push_neg at hP1 hP2 hP3 hP4 set A : ℝ := ‖u₀‖ with hA set B : ℝ := ‖v₀‖ with hB set Q : ℝ := ‖q‖ with hQ have hApos : (0 : ℝ) < A := hu₀pos have hBpos : (0 : ℝ) < B := hv₀pos have hQpos : (0 : ℝ) < Q := hqpos have hP1' : A * B ≤ Q := by have hnorm : ‖u₀ * v₀‖ = A * B := norm_mul _ _ rw [← hnorm]; exact hP1 have hP2' : A * (Q / B) ≤ Q := by have hnorm : ‖u₀ * v₁‖ = A * (Q / B) := by rw [norm_mul, hv₁norm] rw [← hnorm]; exact hP2 have hP3' : (Q / A) * B ≤ Q := by have hnorm : ‖u₁ * v₀‖ = (Q / A) * B := by rw [norm_mul, hu₁norm] rw [← hnorm]; exact hP3 have hP4' : (Q / A) * (Q / B) ≤ Q := by have hnorm : ‖u₁ * v₁‖ = (Q / A) * (Q / B) := by rw [norm_mul, hu₁norm, hv₁norm] rw [← hnorm]; exact hP4 have h4 : Q * Q ≤ Q * (A * B) := by have h := hP4' rw [div_mul_div_comm, div_le_iff₀ (mul_pos hApos hBpos)] at h exact h have hQle : Q ≤ A * B := le_of_mul_le_mul_left h4 hQpos have hAB : A * B = Q := le_antisymm hP1' hQle have h2 : A * Q ≤ Q * B := by have h := hP2' rw [← mul_div_assoc, div_le_iff₀ hBpos] at h exact h have h3 : Q * B ≤ Q * A := by have h := hP3' rw [div_mul_eq_mul_div, div_le_iff₀ hApos] at h exact h have heqnorm : A = B := by nlinarith have hsq : A ^ 2 = Q := by nlinarith have hu₀pow : u₀ ^ p = q ^ (a * (p : ℤ) + su) := by rw [hu₀def, mul_pow, ← zpow_natCast (q ^ a) p, ← zpow_mul, hpu, ← zpow_add₀ hq0] have hnorm_pow : A ^ p = Q ^ (a * (p : ℤ) + su) := by have h := congrArg norm hu₀pow rw [norm_pow, norm_zpow] at h exact h have hexp : (a * (p : ℤ) + su) * 2 = ((p : ℕ) : ℤ) := by have hQ1 : Q ≠ 1 := ne_of_lt hqR have h1 : (Q ^ (a * (p : ℤ) + su)) ^ (2 : ℕ) = Q ^ ((p : ℕ) : ℤ) := by rw [← hnorm_pow, ← pow_mul, mul_comm p 2, pow_mul, hsq, zpow_natCast] have h2 : Q ^ ((a * (p : ℤ) + su) * 2) = Q ^ ((p : ℕ) : ℤ) := by rw [zpow_mul, show ((2 : ℤ)) = ((2 : ℕ) : ℤ) by norm_num, zpow_natCast] exact h1 exact (zpow_right_inj₀ hQpos hQ1).mp h2 rcases hodd with ⟨t, ht⟩ omega end Fiber section TwoTorsion lemma two_nsmul_point_ne_zero (hyps : SymAddHyps q) (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) (hu2 : OffLattice q (u ^ 2)) (hns : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) : (2 : ℕ) • (Point.some (pointX q u) (pointY q u) hns : (curve q).toAffine.Point) ≠ 0 := by intro h2 rw [two_nsmul] at h2 by_cases hy : pointY q u = (curve q).toAffine.negY (pointX q u) (pointY q u) · have hΨ : ((curve q).toAffine.Ψ₂Sq).eval (pointX q u) = 0 := by have hsq := WeierstrassCurve.Affine.sq_sub_negY_eq_eval_Ψ₂Sq (W := (curve q).toAffine) hns.left have h0 : pointY q u - (curve q).toAffine.negY (pointX q u) (pointY q u) = 0 := sub_eq_zero.mpr hy rw [h0] at hsq simpa using hsq.symm have hΦ : (((curve q).toAffine.Φ 2)).eval (pointX q u) = 0 := by have hser : pointX q (u ^ 2) * ((curve q).toAffine.Ψ₂Sq).eval (pointX q u) = (((curve q).toAffine.Φ 2)).eval (pointX q u) := hyps.dbl u hu0 hu hu2 rw [hΨ, mul_zero] at hser exact hser.symm have hΔ : (curve q).Δ ^ 2 = 0 := WeierstrassCurve.Δ_sq_eq_zero_of_eval_eq_zero (W := curve q) hΦ hΨ exact pow_ne_zero 2 (Δ_ne_zero hq0 hq) hΔ · rw [Point.add_self_of_Y_ne hy] at h2 exact Point.some_ne_zero _ h2 end TwoTorsion section Consumers theorem forall_nsmul_ne_zero_of_pow_lattice (hyps : SymAddHyps q) (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) {p : ℕ} {s : ℤ} (hpow : u ^ p = q ^ s) (hp : p.Prime) (hodd : Odd p) (hns : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) : ∀ m : ℕ, 2 ≤ m → m ≤ p - 1 → m • (Point.some (pointX q u) (pointY q u) hns : (curve q).toAffine.Point) ≠ 0 := by set P : (curve q).toAffine.Point := Point.some (pointX q u) (pointY q u) hns with hP have hp3 : 3 ≤ p := by have h2 := hp.two_le rcases hodd with ⟨t, ht⟩ omega intro m induction m using Nat.strong_induction_on with | _ m ih => intro hm2 hmp hm0 have hoffj : ∀ j : ℕ, 1 ≤ j → j ≤ p - 1 → OffLattice q (u ^ j) := fun j hj1 hj2 => offLattice_pow_of_prime hq0 hu0 hu hpow hp (by omega) (by omega) rcases eq_or_lt_of_le hm2 with hm2' | hm3 · have hu2 : OffLattice q (u ^ 2) := hoffj 2 (by omega) (by omega) refine two_nsmul_point_ne_zero hyps hq0 hq hu0 hu hu2 hns ?_ rw [hm2'] rw [hP] at hm0 exact hm0 · have htor' : ∀ m' : ℕ, 2 ≤ m' → m' ≤ m - 1 → m' • (Point.some (pointX q u) (pointY q u) hns : (curve q).toAffine.Point) ≠ 0 := fun m' hm'2 hm'le => ih m' (by omega) hm'2 (by omega) have hoff' : ∀ j : ℕ, 1 ≤ j → j ≤ m - 1 → OffLattice q (u ^ j) := fun j hj1 hj2 => hoffj j hj1 (by omega) have halign := xOrZero_nsmul_of_forall_ne_zero hyps hq0 hu0 hoff' hns htor' obtain ⟨hne, hx⟩ := halign (m - 1) (by omega) le_rfl have hsucc : m • P = (m - 1) • P + P := by conv_lhs => rw [show m = (m - 1) + 1 by omega] exact succ_nsmul P (m - 1) have hneg : (m - 1) • P = -P := by have h0 : (m - 1) • P + P = 0 := by rw [← hsucc]; exact hm0 exact eq_neg_of_add_eq_zero_left h0 have hXcoin : pointX q (u ^ (m - 1)) = pointX q u := by have hx' := hx rw [← hP] at hx' rw [hneg, hP, Point.neg_some, Point.xOrZero_some] at hx' exact hx'.symm have hcast : ((m - 1 : ℕ) : ℤ) = (m : ℤ) - 1 := by omega have hupow : (u ^ (m - 1)) ^ p = q ^ (s * ((m : ℤ) - 1)) := by rw [← pow_mul, mul_comm (m - 1) p, pow_mul, hpow, ← zpow_natCast (q ^ s) (m - 1), ← zpow_mul, hcast] have hoffm1 : OffLattice q (u ^ (m - 1)) := hoffj (m - 1) (by omega) (by omega) rcases exists_zpow_of_pointX_eq_of_pow_lattice hq0 hq (pow_ne_zero _ hu0) hu0 hoffm1 hu hodd hupow hpow hXcoin with ⟨k, hk⟩ | ⟨k, hk⟩ · have hm2off : OffLattice q (u ^ (m - 2)) := hoffj (m - 2) (by omega) (by omega) refine hm2off k ?_ have hsplit : u ^ (m - 1) = u ^ (m - 2) * u := by conv_lhs => rw [show m - 1 = (m - 2) + 1 by omega] rw [pow_succ] have h1 : (q ^ k * u ^ (m - 2)) * u = 1 * u := by rw [one_mul, mul_assoc, ← hsplit, ← hk] exact mul_right_cancel₀ hu0 h1 · have hmoff : OffLattice q (u ^ m) := hoffj m (by omega) (by omega) refine hmoff (-k) ?_ have hsplit : u ^ (m - 1) * u = u ^ m := by conv_rhs => rw [show m = (m - 1) + 1 by omega] rw [pow_succ] rw [← hsplit, hk, ← zpow_add₀ hq0, neg_add_cancel, zpow_zero] theorem nsmul_prime_eq_zero (hyps : SymAddHyps q) (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) {p : ℕ} {s : ℤ} (hpow : u ^ p = q ^ s) (hp : p.Prime) (hodd : Odd p) (hns : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) : p • (Point.some (pointX q u) (pointY q u) hns : (curve q).toAffine.Point) = 0 := nsmul_prime_eq_zero_of_forall_ne_zero hyps hq0 hu0 hu hpow hp hodd hns (forall_nsmul_ne_zero_of_pow_lattice hyps hq0 hq hu0 hu hpow hp hodd hns) theorem eq_zpow_mul_of_pointXY_eq (hyps : SymAddHyps q) (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu : OffLattice q u) (hv : OffLattice q v) {p : ℕ} {su sv : ℤ} (hpu : u ^ p = q ^ su) (hpv : v ^ p = q ^ sv) (hp : p.Prime) (hodd : Odd p) (hX : pointX q u = pointX q v) (hY : pointY q u = pointY q v) : ∃ k : ℤ, v = q ^ k * u := by rcases exists_zpow_of_pointX_eq_of_pow_lattice hq0 hq hu0 hv0 hu hv hodd hpu hpv hX with ⟨k, hk⟩ | ⟨k, hk⟩ · exact ⟨k, hk⟩ · exfalso have hp3 : 3 ≤ p := by have h2 := hp.two_le rcases hodd with ⟨t, ht⟩ omega have hveq : v = q ^ k * u⁻¹ := by have h1 : u⁻¹ * (u * v) = u⁻¹ * q ^ k := by rw [hk] rw [← mul_assoc, inv_mul_cancel₀ hu0, one_mul] at h1 rw [h1, mul_comm] have hXv : pointX q v = pointX q u := by rw [hveq, pointX_zpow_mul hq0, pointX_inv hq0 hu0 hu] have hYv : pointY q v = -pointY q u - pointX q u := by rw [hveq, pointY_zpow_mul hq0, pointY_inv hq0 hq hu0 hu] have hYneg : pointY q u = -pointY q u - pointX q u := by rw [← hYv, ← hY] have hyneg : pointY q u = (curve q).toAffine.negY (pointX q u) (pointY q u) := by show pointY q u = -pointY q u - (curve q).a₁ * pointX q u - (curve q).a₃ rw [curve_a₁, curve_a₃] linear_combination hYneg have hu2 : OffLattice q (u ^ 2) := offLattice_pow_of_prime hq0 hu0 hu hpu hp (by omega) (by omega) have hns : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u) := nonsingular_point hq0 hq hu0 hu have hΨ : ((curve q).toAffine.Ψ₂Sq).eval (pointX q u) = 0 := by have hsq := WeierstrassCurve.Affine.sq_sub_negY_eq_eval_Ψ₂Sq (W := (curve q).toAffine) hns.left have h0 : pointY q u - (curve q).toAffine.negY (pointX q u) (pointY q u) = 0 := sub_eq_zero.mpr hyneg rw [h0] at hsq simpa using hsq.symm have hΦ : (((curve q).toAffine.Φ 2)).eval (pointX q u) = 0 := by have hser : pointX q (u ^ 2) * ((curve q).toAffine.Ψ₂Sq).eval (pointX q u) = (((curve q).toAffine.Φ 2)).eval (pointX q u) := hyps.dbl u hu0 hu hu2 rw [hΨ, mul_zero] at hser exact hser.symm have hΔ : (curve q).Δ ^ 2 = 0 := WeierstrassCurve.Δ_sq_eq_zero_of_eval_eq_zero (W := curve q) hΦ hΨ exact pow_ne_zero 2 (Δ_ne_zero hq0 hq) hΔ lemma pointXY_eq_of_zpow_mul (hq0 : q ≠ 0) (k : ℤ) : pointX q (q ^ k * u) = pointX q u ∧ pointY q (q ^ k * u) = pointY q u := ⟨pointX_zpow_mul hq0 k, pointY_zpow_mul hq0 k⟩ end Consumers end TateCurve open Polynomial open scoped NNReal namespace TateCurve variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [CharZero K] [DecidableEq K] variable {q u : K} lemma symSumNum_self (z : K) : symSumNum q z z = ((curve q).Ψ₂Sq).eval z := by rw [WeierstrassCurve.Affine.eval_Ψ₂Sq, curve_b₂, curve_b₄, curve_b₆] simp only [symSumNum]; ring lemma symProdNum_self (z : K) : symProdNum q z z = ((curve q).Φ 2).eval z := by rw [WeierstrassCurve.Affine.eval_Φ_two, curve_b₄, curve_b₆, curve_b₈] simp only [symProdNum]; ring private lemma not_both_eval_eq_zero (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {z : K} (h1 : ((curve q).Ψ₂Sq).eval z = 0) (h2 : ((curve q).Φ 2).eval z = 0) : False := by haveI := isElliptic hq0 hq exact (curve q).not_eval_Φ_two_eq_zero h1 h2 private lemma quad_transfer (x y s t : K) (h3 : (s + t) * (x - y) ^ 2 = symSumNum q x y) (h4 : s * t * (x - y) ^ 2 = symProdNum q x y) : (symProdNum q s t * (((curve q).Ψ₂Sq).eval x) ^ 2 - symSumNum q s t * (((curve q).Ψ₂Sq).eval x) * (((curve q).Φ 2).eval x) + (s - t) ^ 2 * (((curve q).Φ 2).eval x) ^ 2) * ((x - y) ^ 2) ^ 2 = 0 := by have hΨ : ((curve q).Ψ₂Sq).eval x = 4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q := by rw [WeierstrassCurve.Affine.eval_Ψ₂Sq, curve_b₂, curve_b₄, curve_b₆]; ring have hΦ : ((curve q).Φ 2).eval x = x ^ 4 - 2 * a₄ q * x ^ 2 - 8 * a₆ q * x - a₆ q + a₄ q ^ 2 := by rw [WeierstrassCurve.Affine.eval_Φ_two, curve_b₄, curve_b₆, curve_b₈]; ring rw [hΨ, hΦ] simp only [symSumNum, symProdNum] at h3 h4 ⊢ linear_combination ((x ^ 4 - 2 * a₄ q * x ^ 2 - 8 * a₆ q * x - a₆ q + a₄ q ^ 2) ^ 2 * ((s + t) * (x - y) ^ 2 + (2 * (x * y) * (x + y) + x * y + 2 * a₄ q * (x + y) + 4 * a₆ q)) - 4 * a₆ q * (x - y) ^ 2 * (4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q) ^ 2 - 2 * (s * t * (x - y) ^ 2) * (4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q) * (x ^ 4 - 2 * a₄ q * x ^ 2 - 8 * a₆ q * x - a₆ q + a₄ q ^ 2) - 2 * a₄ q * (x - y) ^ 2 * (4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q) * (x ^ 4 - 2 * a₄ q * x ^ 2 - 8 * a₆ q * x - a₆ q + a₄ q ^ 2)) * h3 + ((4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q) ^ 2 * (s * t * (x - y) ^ 2 + ((x * y) ^ 2 - 2 * a₄ q * (x * y) - 4 * a₆ q * (x + y) - a₆ q + a₄ q ^ 2)) - 2 * a₄ q * (x - y) ^ 2 * (4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q) ^ 2 - (2 * (2 * (x * y) * (x + y) + x * y + 2 * a₄ q * (x + y) + 4 * a₆ q) + (x - y) ^ 2) * (4 * x ^ 3 + x ^ 2 + 4 * a₄ q * x + 4 * a₆ q) * (x ^ 4 - 2 * a₄ q * x ^ 2 - 8 * a₆ q * x - a₆ q + a₄ q ^ 2) - 4 * (x - y) ^ 2 * (x ^ 4 - 2 * a₄ q * x ^ 2 - 8 * a₆ q * x - a₆ q + a₄ q ^ 2) ^ 2) * h4 section AuxiliarySupply private structure DiamondAux (q u w : K) : Prop where ne_zero : w ≠ 0 nnnorm_eq : ‖w‖₊ = 1 offLattice : OffLattice q w offLattice_sq : OffLattice q (w ^ 2) offLattice_mul : OffLattice q (u * w) offLattice_div : OffLattice q (u * w⁻¹) private lemma nnnorm_pow_lt_one (hq : ‖q‖₊ < 1) {n : ℕ} (hn : 1 ≤ n) : ‖q ^ n‖₊ < 1 := by rw [nnnorm_pow] exact pow_lt_one₀ zero_le hq (by omega) private lemma nnnorm_one_add_pow (hq : ‖q‖₊ < 1) {n : ℕ} (hn : 1 ≤ n) : ‖(1 : K) + q ^ n‖₊ = 1 := by have h : ((1 : K) + q ^ n) = 1 - (-(q ^ n)) := by ring rw [h] refine nnnorm_one_sub_of_lt_one ?_ rw [nnnorm_neg] exact nnnorm_pow_lt_one hq hn private lemma one_add_pow_ne_zero (hq : ‖q‖₊ < 1) {n : ℕ} (hn : 1 ≤ n) : (1 : K) + q ^ n ≠ 0 := by intro h0 have := nnnorm_one_add_pow (q := q) hq hn rw [h0, nnnorm_zero] at this exact zero_ne_one this private lemma one_add_pow_ne_one (hq0 : q ≠ 0) {n : ℕ} (hn : 1 ≤ n) : (1 : K) + q ^ n ≠ 1 := by intro h have hpow : q ^ n = 0 := by linear_combination h exact hq0 (pow_eq_zero_iff (by omega) |>.mp hpow) private lemma offLattice_of_nnnorm_eq_one (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {w : K} (hw : ‖w‖₊ = 1) (hw1 : w ≠ 1) : OffLattice q w := by intro k hk have hnorm : ‖q‖₊ ^ k * ‖w‖₊ = 1 := by have := congrArg (‖·‖₊) hk simpa [nnnorm_mul, nnnorm_zpow] using this have hk0 : k = 0 := by have hq_pos : (0 : ℝ≥0) < ‖q‖₊ := by simpa [pos_iff_ne_zero, nnnorm_eq_zero] using hq0 have : ‖q‖₊ ^ k = ‖q‖₊ ^ (0 : ℤ) := by rw [zpow_zero] rw [hw, mul_one] at hnorm exact hnorm exact zpow_right_injective₀ hq_pos (ne_of_lt hq) this rw [hk0, zpow_zero, one_mul] at hk exact hw1 hk private lemma one_add_pow_injective (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {n m : ℕ} (h : (1 : K) + q ^ n = 1 + q ^ m) : n = m := by have hpow : q ^ n = q ^ m := by linear_combination h have hnorm : ‖q‖₊ ^ (n : ℤ) = ‖q‖₊ ^ (m : ℤ) := by rw [zpow_natCast, zpow_natCast, ← nnnorm_pow, ← nnnorm_pow, hpow] have hq_pos : (0 : ℝ≥0) < ‖q‖₊ := by simpa [pos_iff_ne_zero, nnnorm_eq_zero] using hq0 have := zpow_right_injective₀ hq_pos (ne_of_lt hq) hnorm exact_mod_cast this private lemma one_add_pow_mul_ne_one (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {n m : ℕ} (hn : 1 ≤ n) (hnm : n < m) : ((1 : K) + q ^ n) * (1 + q ^ m) ≠ 1 := by intro h have hmn : n + (m - n) = m := by omega have key : q ^ n * (1 + (q ^ (m - n) + q ^ m)) = 0 := by have expand : q ^ n * (1 + (q ^ (m - n) + q ^ m)) = q ^ n + (q ^ (n + (m - n)) + q ^ (n + m)) := by rw [pow_add, pow_add]; ring rw [expand, hmn] linear_combination h have h2 : (1 : K) + (q ^ (m - n) + q ^ m) = 0 := by rcases mul_eq_zero.mp key with h' | h' · exact absurd (pow_eq_zero_iff (by omega) |>.mp h') hq0 · exact h' have hsmall : ‖q ^ (m - n) + q ^ m‖₊ < 1 := by refine lt_of_le_of_lt (IsUltrametricDist.nnnorm_add_le_max _ _) ?_ exact max_lt (nnnorm_pow_lt_one hq (by omega)) (nnnorm_pow_lt_one hq (by omega)) have hone : ‖(1 : K) + (q ^ (m - n) + q ^ m)‖₊ = 1 := by have h' : ((1 : K) + (q ^ (m - n) + q ^ m)) = 1 - (-(q ^ (m - n) + q ^ m)) := by ring rw [h'] exact nnnorm_one_sub_of_lt_one (by rwa [nnnorm_neg]) rw [h2, nnnorm_zero] at hone exact zero_ne_one hone private lemma lattice_mul_unique (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (h1 : ¬ OffLattice q (u * (1 + q ^ n))) (h2 : ¬ OffLattice q (u * (1 + q ^ m))) : n = m := by simp only [OffLattice, not_forall, not_not] at h1 h2 obtain ⟨k, hk⟩ := h1 obtain ⟨j, hj⟩ := h2 have hcn := nnnorm_one_add_pow (q := q) hq hn have hcm := nnnorm_one_add_pow (q := q) hq hm have hq_pos : (0 : ℝ≥0) < ‖q‖₊ := by simpa [pos_iff_ne_zero, nnnorm_eq_zero] using hq0 have hu_ne : ‖u‖₊ ≠ 0 := by simpa [nnnorm_eq_zero] using hu0 have hnk : ‖q‖₊ ^ k * ‖u‖₊ = 1 := by have := congrArg (‖·‖₊) hk simpa [nnnorm_mul, nnnorm_zpow, hcn, mul_assoc] using this have hnj : ‖q‖₊ ^ j * ‖u‖₊ = 1 := by have := congrArg (‖·‖₊) hj simpa [nnnorm_mul, nnnorm_zpow, hcm, mul_assoc] using this have hkj : k = j := by have : ‖q‖₊ ^ k = ‖q‖₊ ^ j := by have := hnk.trans hnj.symm exact mul_right_cancel₀ hu_ne this exact zpow_right_injective₀ hq_pos (ne_of_lt hq) this rw [hkj] at hk have hcancel : (1 : K) + q ^ n = 1 + q ^ m := by have hqu : (q : K) ^ j * u ≠ 0 := mul_ne_zero (zpow_ne_zero _ hq0) hu0 apply mul_left_cancel₀ hqu calc q ^ j * u * (1 + q ^ n) = q ^ j * (u * (1 + q ^ n)) := by ring _ = 1 := hk _ = q ^ j * (u * (1 + q ^ m)) := hj.symm _ = q ^ j * u * (1 + q ^ m) := by ring exact one_add_pow_injective hq0 hq hcancel private lemma lattice_div_unique (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (h1 : ¬ OffLattice q (u * (1 + q ^ n)⁻¹)) (h2 : ¬ OffLattice q (u * (1 + q ^ m)⁻¹)) : n = m := by simp only [OffLattice, not_forall, not_not] at h1 h2 obtain ⟨k, hk⟩ := h1 obtain ⟨j, hj⟩ := h2 have hcn := nnnorm_one_add_pow (q := q) hq hn have hcm := nnnorm_one_add_pow (q := q) hq hm have hcn0 := one_add_pow_ne_zero (q := q) hq hn have hcm0 := one_add_pow_ne_zero (q := q) hq hm have hq_pos : (0 : ℝ≥0) < ‖q‖₊ := by simpa [pos_iff_ne_zero, nnnorm_eq_zero] using hq0 have hu_ne : ‖u‖₊ ≠ 0 := by simpa [nnnorm_eq_zero] using hu0 have hnk : ‖q‖₊ ^ k * ‖u‖₊ = 1 := by have := congrArg (‖·‖₊) hk simpa [nnnorm_mul, nnnorm_zpow, nnnorm_inv, hcn, mul_assoc] using this have hnj : ‖q‖₊ ^ j * ‖u‖₊ = 1 := by have := congrArg (‖·‖₊) hj simpa [nnnorm_mul, nnnorm_zpow, nnnorm_inv, hcm, mul_assoc] using this have hkj : k = j := by have : ‖q‖₊ ^ k = ‖q‖₊ ^ j := by have := hnk.trans hnj.symm exact mul_right_cancel₀ hu_ne this exact zpow_right_injective₀ hq_pos (ne_of_lt hq) this rw [hkj] at hk have hcancel : ((1 : K) + q ^ n)⁻¹ = (1 + q ^ m)⁻¹ := by have hqu : (q : K) ^ j * u ≠ 0 := mul_ne_zero (zpow_ne_zero _ hq0) hu0 apply mul_left_cancel₀ hqu calc q ^ j * u * (1 + q ^ n)⁻¹ = q ^ j * (u * (1 + q ^ n)⁻¹) := by ring _ = 1 := hk _ = q ^ j * (u * (1 + q ^ m)⁻¹) := hj.symm _ = q ^ j * u * (1 + q ^ m)⁻¹ := by ring exact one_add_pow_injective hq0 hq (by have := congrArg (·⁻¹) hcancel simpa [inv_inv] using this) private lemma pair_bad_unique (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {a m m' : ℕ} (ha : 1 ≤ a) (hm : 1 ≤ m) (hm' : 1 ≤ m') (h1 : (1 : K) + q ^ a = -(1 + q ^ m) ∨ ((1 : K) + q ^ a) * (1 + q ^ m) = -1) (h2 : (1 : K) + q ^ a = -(1 + q ^ m') ∨ ((1 : K) + q ^ a) * (1 + q ^ m') = -1) : m = m' := by have ha0 := one_add_pow_ne_zero (q := q) hq ha rcases h1 with h1 | h1 <;> rcases h2 with h2 | h2 · have hmm' : (1 : K) + q ^ m = 1 + q ^ m' := by have h12 := h1.symm.trans h2 linear_combination -h12 exact one_add_pow_injective hq0 hq hmm' · by_contra hne have hprod : ((1 : K) + q ^ m) * (1 + q ^ m') = 1 := by have hmul : (-(1 + q ^ m) : K) * (1 + q ^ m') = -1 := by rw [← h1]; exact h2 linear_combination -hmul rcases lt_or_gt_of_ne hne with hlt | hlt · exact one_add_pow_mul_ne_one hq0 hq hm hlt hprod · exact one_add_pow_mul_ne_one hq0 hq hm' hlt (by linear_combination hprod) · by_contra hne have hprod : ((1 : K) + q ^ m) * (1 + q ^ m') = 1 := by have hmul : (-(1 + q ^ m') : K) * (1 + q ^ m) = -1 := by rw [← h2]; exact h1 linear_combination -hmul rcases lt_or_gt_of_ne hne with hlt | hlt · exact one_add_pow_mul_ne_one hq0 hq hm hlt hprod · exact one_add_pow_mul_ne_one hq0 hq hm' hlt (by linear_combination hprod) · have : (1 : K) + q ^ m = 1 + q ^ m' := by apply mul_left_cancel₀ ha0 rw [h1, h2] exact one_add_pow_injective hq0 hq this private lemma diamondAux_of_good (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {u : K} {n : ℕ} (hn : 1 ≤ n) (hneg : (1 : K) + q ^ n ≠ -1) (hmul : OffLattice q (u * (1 + q ^ n))) (hdiv : OffLattice q (u * (1 + q ^ n)⁻¹)) : DiamondAux q u (1 + q ^ n) := by have hw0 := one_add_pow_ne_zero (q := q) hq hn have hw1 := one_add_pow_ne_one (q := q) hq0 hn have hwn := nnnorm_one_add_pow (q := q) hq hn refine ⟨hw0, hwn, offLattice_of_nnnorm_eq_one hq0 hq hwn hw1, ?_, hmul, hdiv⟩ refine offLattice_of_nnnorm_eq_one hq0 hq (by rw [nnnorm_pow, hwn, one_pow]) ?_ intro hsq have hfact : (((1 : K) + q ^ n) - 1) * ((1 + q ^ n) + 1) = 0 := by linear_combination hsq rcases mul_eq_zero.mp hfact with h' | h' · exact hw1 (by linear_combination h') · exact hneg (by linear_combination h') private lemma exists_diamond_aux (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {u : K} (hu0 : u ≠ 0) : ∃ w₁ w₂ : K, DiamondAux q u w₁ ∧ DiamondAux q u w₂ ∧ w₁ ^ 2 ≠ w₂ ^ 2 ∧ w₁ ^ 2 * w₂ ^ 2 ≠ 1 := by classical have pick₁ : ∃ n : ℕ, (1 ≤ n ∧ n ≤ 4) ∧ ((1 : K) + q ^ n ≠ -1) ∧ OffLattice q (u * (1 + q ^ n)) ∧ OffLattice q (u * (1 + q ^ n)⁻¹) := by have hgood : ∃ n ∈ Finset.Icc 1 4, n ∉ (((Finset.Icc 1 4).filter fun n => (1 : K) + q ^ n = -1) ∪ ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n))) ∪ ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n)⁻¹))) := by by_contra hall push_neg at hall have hsub : Finset.Icc 1 4 ⊆ (((Finset.Icc 1 4).filter fun n => (1 : K) + q ^ n = -1) ∪ ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n))) ∪ ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n)⁻¹))) := fun n hn => hall n hn have hcard := Finset.card_le_card hsub have hc₁ : ((Finset.Icc 1 4).filter fun n => (1 : K) + q ^ n = -1).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter] at ha hb exact one_add_pow_injective hq0 hq (ha.2.trans hb.2.symm) have hc₂ : ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n))).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter, Finset.mem_Icc] at ha hb exact lattice_mul_unique hq0 hq hu0 ha.1.1 hb.1.1 ha.2 hb.2 have hc₃ : ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n)⁻¹)).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter, Finset.mem_Icc] at ha hb exact lattice_div_unique hq0 hq hu0 ha.1.1 hb.1.1 ha.2 hb.2 have hpair := Finset.card_union_le ((Finset.Icc 1 4).filter fun n => (1 : K) + q ^ n = -1) ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n))) have htriple := Finset.card_union_le (((Finset.Icc 1 4).filter fun n => (1 : K) + q ^ n = -1) ∪ ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n)))) ((Finset.Icc 1 4).filter fun n => ¬ OffLattice q (u * (1 + q ^ n)⁻¹)) rw [Nat.card_Icc] at hcard omega obtain ⟨n, hnmem, hnot⟩ := hgood have hn := Finset.mem_Icc.mp hnmem simp only [Finset.mem_union, Finset.mem_filter, not_or, not_and, not_not] at hnot exact ⟨n, hn, hnot.1.1 hnmem, hnot.1.2 hnmem, hnot.2 hnmem⟩ obtain ⟨n₁, hn₁, hg₁neg, hg₁mul, hg₁div⟩ := pick₁ have pick₂ : ∃ m : ℕ, (n₁ + 1 ≤ m ∧ m ≤ n₁ + 5) ∧ ((1 : K) + q ^ m ≠ -1) ∧ OffLattice q (u * (1 + q ^ m)) ∧ OffLattice q (u * (1 + q ^ m)⁻¹) ∧ ¬((1 : K) + q ^ n₁ = -(1 + q ^ m) ∨ ((1 : K) + q ^ n₁) * (1 + q ^ m) = -1) := by have hgood : ∃ m ∈ Finset.Icc (n₁ + 1) (n₁ + 5), m ∉ ((((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ m = -1) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m))) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)⁻¹))) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ n₁ = -(1 + q ^ m) ∨ ((1 : K) + q ^ n₁) * (1 + q ^ m) = -1)) := by by_contra hall push_neg at hall have hsub : Finset.Icc (n₁ + 1) (n₁ + 5) ⊆ ((((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ m = -1) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m))) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)⁻¹))) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ n₁ = -(1 + q ^ m) ∨ ((1 : K) + q ^ n₁) * (1 + q ^ m) = -1)) := fun m hm => hall m hm have hcard := Finset.card_le_card hsub have hc₁ : ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ m = -1).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter] at ha hb exact one_add_pow_injective hq0 hq (ha.2.trans hb.2.symm) have hc₂ : ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m))).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter, Finset.mem_Icc] at ha hb exact lattice_mul_unique hq0 hq hu0 (by omega) (by omega) ha.2 hb.2 have hc₃ : ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)⁻¹)).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter, Finset.mem_Icc] at ha hb exact lattice_div_unique hq0 hq hu0 (by omega) (by omega) ha.2 hb.2 have hc₄ : ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ n₁ = -(1 + q ^ m) ∨ ((1 : K) + q ^ n₁) * (1 + q ^ m) = -1).card ≤ 1 := Finset.card_le_one.mpr fun a ha b hb => by rw [Finset.mem_filter, Finset.mem_Icc] at ha hb exact pair_bad_unique hq0 hq hn₁.1 (by omega) (by omega) ha.2 hb.2 have hpairc := Finset.card_union_le ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ m = -1) ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m))) have htriple := Finset.card_union_le (((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ m = -1) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)))) ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)⁻¹)) have hquad := Finset.card_union_le ((((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ m = -1) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)))) ∪ ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => ¬ OffLattice q (u * (1 + q ^ m)⁻¹))) ((Finset.Icc (n₁ + 1) (n₁ + 5)).filter fun m => (1 : K) + q ^ n₁ = -(1 + q ^ m) ∨ ((1 : K) + q ^ n₁) * (1 + q ^ m) = -1) rw [Nat.card_Icc] at hcard omega obtain ⟨m, hmmem, hnot⟩ := hgood have hm := Finset.mem_Icc.mp hmmem simp only [Finset.mem_union, Finset.mem_filter, not_or, not_and, not_not] at hnot refine ⟨m, hm, hnot.1.1.1 hmmem, hnot.1.1.2 hmmem, hnot.1.2 hmmem, ?_⟩ intro hbad rcases hbad with hbad | hbad · exact (hnot.2 hmmem).1 hbad · exact (hnot.2 hmmem).2 hbad obtain ⟨n₂, hn₂, hg₂neg, hg₂mul, hg₂div, hpairgood⟩ := pick₂ push_neg at hpairgood have hn₂1 : 1 ≤ n₂ := by omega have hne : n₁ ≠ n₂ := by omega refine ⟨1 + q ^ n₁, 1 + q ^ n₂, diamondAux_of_good hq0 hq hn₁.1 hg₁neg hg₁mul hg₁div, diamondAux_of_good hq0 hq hn₂1 hg₂neg hg₂mul hg₂div, ?_, ?_⟩ · intro hsq have hfact : (((1 : K) + q ^ n₁) - (1 + q ^ n₂)) * ((1 + q ^ n₁) + (1 + q ^ n₂)) = 0 := by linear_combination hsq rcases mul_eq_zero.mp hfact with h' | h' · exact hne (one_add_pow_injective hq0 hq (by linear_combination h')) · exact hpairgood.1 (by linear_combination h') · intro hsq have hfact : (((1 : K) + q ^ n₁) * (1 + q ^ n₂) - 1) * ((1 + q ^ n₁) * (1 + q ^ n₂) + 1) = 0 := by linear_combination hsq rcases mul_eq_zero.mp hfact with h' | h' · have hone : ((1 : K) + q ^ n₁) * (1 + q ^ n₂) = 1 := by linear_combination h' exact one_add_pow_mul_ne_one hq0 hq hn₁.1 (by omega) hone · exact hpairgood.2 (by linear_combination h') end AuxiliarySupply private lemma diamond_branch (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hsum : ∀ u v : K, AddParams q u v → (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hprod : ∀ u v : K, AddParams q u v → pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v)) {u w : K} (hu0 : u ≠ 0) (hu : OffLattice q u) (hu2 : OffLattice q (u ^ 2)) (hw : DiamondAux q u w) : pointX q (u ^ 2) * ((curve q).Ψ₂Sq).eval (pointX q u) = ((curve q).Φ 2).eval (pointX q u) ∨ ((curve q).Φ 2).eval (pointX q u) = pointX q (w ^ 2) * ((curve q).Ψ₂Sq).eval (pointX q u) := by have hw0 : w ≠ 0 := hw.ne_zero have hAPA : AddParams q u w := ⟨hq0, hu0, hw0, hu, hw.offLattice, hw.offLattice_mul, hw.offLattice_div⟩ have hmul0 : u * w ≠ 0 := mul_ne_zero hu0 hw0 have hdiv0 : u * w⁻¹ ≠ 0 := mul_ne_zero hu0 (inv_ne_zero hw0) have hBmul : (u * w) * (u * w⁻¹) = u ^ 2 := by field_simp have hBdiv : (u * w) * (u * w⁻¹)⁻¹ = w ^ 2 := by rw [mul_inv, inv_inv] field_simp have hAPB : AddParams q (u * w) (u * w⁻¹) := by refine ⟨hq0, hmul0, hdiv0, hw.offLattice_mul, hw.offLattice_div, ?_, ?_⟩ · rw [hBmul]; exact hu2 · rw [hBdiv]; exact hw.offLattice_sq have hA1 := hsum u w hAPA have hA2 := hprod u w hAPA have hB1 := hsum (u * w) (u * w⁻¹) hAPB have hB2 := hprod (u * w) (u * w⁻¹) hAPB rw [hBmul, hBdiv] at hB1 hB2 set x := pointX q u with hxdef set y := pointX q w with hydef set s := pointX q (u * w) with hsdef set t := pointX q (u * w⁻¹) with htdef set D := pointX q (u ^ 2) with hDdef set E := pointX q (w ^ 2) with hEdef set Ψx := ((curve q).Ψ₂Sq).eval x with hΨdef set Φx := ((curve q).Φ 2).eval x with hΦdef have hxy : x ≠ y := by intro hxe have e1 : symSumNum q x y = 0 := by rw [← hA1, hxe]; ring have e2 : symProdNum q x y = 0 := by rw [← hA2, hxe]; ring rw [hxe] at e1 e2 rw [symSumNum_self] at e1 rw [symProdNum_self] at e2 exact not_both_eval_eq_zero hq0 hq e1 e2 have hst : s ≠ t := by intro hse have e1 : symSumNum q s t = 0 := by rw [← hB1, hse]; ring have e2 : symProdNum q s t = 0 := by rw [← hB2, hse]; ring rw [hse] at e1 e2 rw [symSumNum_self] at e1 rw [symProdNum_self] at e2 exact not_both_eval_eq_zero hq0 hq e1 e2 have hG : symProdNum q s t * Ψx ^ 2 - symSumNum q s t * Ψx * Φx + (s - t) ^ 2 * Φx ^ 2 = 0 := by have h := quad_transfer (q := q) x y s t hA1 hA2 have hd2 : ((x - y) ^ 2) ^ 2 ≠ 0 := pow_ne_zero _ (pow_ne_zero _ (sub_ne_zero.mpr hxy)) rcases mul_eq_zero.mp h with h' | h' · exact h' · exact absurd h' hd2 have hfact : (s - t) ^ 2 * ((Φx - D * Ψx) * (Φx - E * Ψx)) = 0 := by linear_combination hG - Ψx * Φx * hB1 + Ψx ^ 2 * hB2 have hst2 : (s - t) ^ 2 ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hst) have hsplit : (Φx - D * Ψx) * (Φx - E * Ψx) = 0 := by rcases mul_eq_zero.mp hfact with h' | h' · exact absurd h' hst2 · exact h' rcases mul_eq_zero.mp hsplit with h' | h' · left; linear_combination -h' · right; linear_combination h' theorem dbl_of_symAdd_sum_prod (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hsum : ∀ u v : K, AddParams q u v → (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hprod : ∀ u v : K, AddParams q u v → pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v)) : ∀ u : K, u ≠ 0 → OffLattice q u → OffLattice q (u ^ 2) → pointX q (u ^ 2) * ((curve q).Ψ₂Sq).eval (pointX q u) = ((curve q).Φ 2).eval (pointX q u) := by intro u hu0 hu hu2 obtain ⟨w₁, w₂, haux₁, haux₂, hsqne, hsqprod⟩ := exists_diamond_aux hq0 hq (u := u) hu0 rcases diamond_branch hq0 hq hsum hprod hu0 hu hu2 haux₁ with hdone | hbad₁ · exact hdone rcases diamond_branch hq0 hq hsum hprod hu0 hu hu2 haux₂ with hdone | hbad₂ · exact hdone have hw₁sq0 : w₁ ^ 2 ≠ 0 := pow_ne_zero _ haux₁.ne_zero have hw₂sq0 : w₂ ^ 2 ≠ 0 := pow_ne_zero _ haux₂.ne_zero have hEne : pointX q (w₁ ^ 2) ≠ pointX q (w₂ ^ 2) := by intro hEq have hnorm₁ : ‖w₁ ^ 2‖ ≤ 1 := by have : ‖w₁ ^ 2‖₊ = 1 := by rw [nnnorm_pow, haux₁.nnnorm_eq, one_pow] simp [← coe_nnnorm, this] have hnorm₂ : ‖w₂ ^ 2‖ ≤ 1 := by have : ‖w₂ ^ 2‖₊ = 1 := by rw [nnnorm_pow, haux₂.nnnorm_eq, one_pow] simp [← coe_nnnorm, this] have hnormprod : ‖q‖ < ‖w₁ ^ 2 * w₂ ^ 2‖ := by have h1 : ‖w₁ ^ 2 * w₂ ^ 2‖₊ = 1 := by rw [nnnorm_mul, nnnorm_pow, nnnorm_pow, haux₁.nnnorm_eq, haux₂.nnnorm_eq] simp have h2 : ‖w₁ ^ 2 * w₂ ^ 2‖ = 1 := by simpa [← coe_nnnorm] using congrArg (NNReal.toReal) h1 rw [h2] exact_mod_cast hq rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hw₁sq0 hw₂sq0 haux₁.offLattice_sq haux₂.offLattice_sq hnorm₁ hnorm₂ hnormprod hEq with h | h · exact hsqne h · exact hsqprod h have hΨ0 : ((curve q).Ψ₂Sq).eval (pointX q u) = 0 := by have hkey : (pointX q (w₁ ^ 2) - pointX q (w₂ ^ 2)) * ((curve q).Ψ₂Sq).eval (pointX q u) = 0 := by linear_combination hbad₂ - hbad₁ rcases mul_eq_zero.mp hkey with h | h · exact absurd (sub_eq_zero.mp h) hEne · exact h have hΦ0 : ((curve q).Φ 2).eval (pointX q u) = 0 := by rw [hbad₁, hΨ0, mul_zero] exact absurd hΦ0 (fun hΦ0 => not_both_eval_eq_zero hq0 hq hΨ0 hΦ0) theorem symAddHyps_of_sum_prod (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hsum : ∀ u v : K, AddParams q u v → (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hprod : ∀ u v : K, AddParams q u v → pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v)) : SymAddHyps q := ⟨hsum, hprod, dbl_of_symAdd_sum_prod hq0 hq hsum hprod⟩ end TateCurve set_option linter.unusedSectionVars false open Polynomial open scoped NNReal namespace TateCurve variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] [CharZero K] [DecidableEq K] variable {q u v : K} theorem two_mul_pointY_add_pointX_sq (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) : (2 * pointY q u + pointX q u) ^ 2 = 4 * pointX q u ^ 3 + pointX q u ^ 2 + 4 * a₄ q * pointX q u + 4 * a₆ q := by have h := equation_pointX_pointY hq0 hq hu0 hu linear_combination 4 * h theorem two_mul_pointY_add_pointX_sq_eq_eval_Ψ₂Sq (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) : (2 * pointY q u + pointX q u) ^ 2 = ((curve q).Ψ₂Sq).eval (pointX q u) := by have hΨ : ((curve q).Ψ₂Sq).eval (pointX q u) = 4 * pointX q u ^ 3 + pointX q u ^ 2 + 4 * a₄ q * pointX q u + 4 * a₆ q := by rw [WeierstrassCurve.Affine.eval_Ψ₂Sq, curve_b₂, curve_b₄, curve_b₆]; ring rw [hΨ] exact two_mul_pointY_add_pointX_sq hq0 hq hu0 hu theorem symSumNum_sq_sub_quartic_mul_quartic (q x₁ x₂ : K) : symSumNum q x₁ x₂ ^ 2 - (4 * x₁ ^ 3 + x₁ ^ 2 + 4 * a₄ q * x₁ + 4 * a₆ q) * (4 * x₂ ^ 3 + x₂ ^ 2 + 4 * a₄ q * x₂ + 4 * a₆ q) = 4 * (x₁ - x₂) ^ 2 * symProdNum q x₁ x₂ := by simp only [symSumNum, symProdNum]; ring section PerPair theorem symAdd_prod_of_sum_of_diff_sq (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) (hv0 : v ≠ 0) (hv : OffLattice q v) (hne : pointX q u ≠ pointX q v) (hsum : (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hdiffsq : ((pointX q (u * v) - pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2) ^ 2 = ((2 * pointY q u + pointX q u) * (2 * pointY q v + pointX q v)) ^ 2) : pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v) := by have hQ1 := two_mul_pointY_add_pointX_sq hq0 hq hu0 hu have hQ2 := two_mul_pointY_add_pointX_sq hq0 hq hv0 hv have hsumsq : ((pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2) ^ 2 = symSumNum q (pointX q u) (pointX q v) ^ 2 := by rw [hsum] have key : (4 : K) * (pointX q u - pointX q v) ^ 2 * (pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 - symProdNum q (pointX q u) (pointX q v)) = 0 := by simp only [symSumNum] at hsumsq simp only [symProdNum] linear_combination hsumsq - hdiffsq - (2 * pointY q v + pointX q v) ^ 2 * hQ1 - (4 * pointX q u ^ 3 + pointX q u ^ 2 + 4 * a₄ q * pointX q u + 4 * a₆ q) * hQ2 have h4 : (4 : K) ≠ 0 := by norm_num have hΔ : (pointX q u - pointX q v) ^ 2 ≠ 0 := pow_ne_zero 2 (sub_ne_zero.mpr hne) rcases mul_eq_zero.mp key with h0 | h0 · exact absurd h0 (mul_ne_zero h4 hΔ) · exact sub_eq_zero.mp h0 theorem symAdd_prod_of_sum_of_diff (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) (hv0 : v ≠ 0) (hv : OffLattice q v) (hne : pointX q u ≠ pointX q v) (hsum : (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hdiff : (pointX q (u * v) - pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = -((2 * pointY q u + pointX q u) * (2 * pointY q v + pointX q v))) : pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v) := symAdd_prod_of_sum_of_diff_sq hq0 hq hu0 hu hv0 hv hne hsum (by rw [hdiff]; ring) theorem symAdd_prod_of_sum_of_diff' (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u) (hv0 : v ≠ 0) (hv : OffLattice q v) (hne : pointX q u ≠ pointX q v) (hsum : (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hdiff : (pointX q (u * v) - pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = (2 * pointY q u + pointX q u) * (2 * pointY q v + pointX q v)) : pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v) := symAdd_prod_of_sum_of_diff_sq hq0 hq hu0 hu hv0 hv hne hsum (by rw [hdiff]) end PerPair section Forall theorem symAdd_prod_of_sum_diff_forall (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hsum : ∀ u v : K, AddParams q u v → (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hdiff : ∀ u v : K, AddParams q u v → (pointX q (u * v) - pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = -((2 * pointY q u + pointX q u) * (2 * pointY q v + pointX q v))) (hsep : ∀ u v : K, AddParams q u v → 2 * pointY q u + pointX q u = 0 → 2 * pointY q v + pointX q v = 0 → pointX q u ≠ pointX q v) : ∀ u v : K, AddParams q u v → pointX q (u * v) * pointX q (u * v⁻¹) * (pointX q u - pointX q v) ^ 2 = symProdNum q (pointX q u) (pointX q v) := by intro u v h by_cases hne : pointX q u = pointX q v · exfalso have hS1 := hsum u v h have hQ1 := two_mul_pointY_add_pointX_sq hq0 hq h.u_ne_zero h.offLattice_u have hQ2 := two_mul_pointY_add_pointX_sq hq0 hq h.v_ne_zero h.offLattice_v have hzero : symSumNum q (pointX q u) (pointX q u) = 0 := by have h2 : (pointX q u - pointX q v) ^ 2 = 0 := by rw [hne]; ring calc symSumNum q (pointX q u) (pointX q u) = symSumNum q (pointX q u) (pointX q v) := by rw [hne] _ = (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 := hS1.symm _ = 0 := by rw [h2, mul_zero] have hpsiu : 2 * pointY q u + pointX q u = 0 := by have hsq : (2 * pointY q u + pointX q u) ^ 2 = 0 := by rw [hQ1] simp only [symSumNum] at hzero linear_combination hzero exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp hsq have hpsiv : 2 * pointY q v + pointX q v = 0 := by have hsq : (2 * pointY q v + pointX q v) ^ 2 = 0 := by rw [hQ2, ← hne] simp only [symSumNum] at hzero linear_combination hzero exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp hsq exact hsep u v h hpsiu hpsiv hne · exact symAdd_prod_of_sum_of_diff hq0 hq h.u_ne_zero h.offLattice_u h.v_ne_zero h.offLattice_v hne (hsum u v h) (hdiff u v h) theorem symAddHyps_of_sum_diff (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hsum : ∀ u v : K, AddParams q u v → (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hdiff : ∀ u v : K, AddParams q u v → (pointX q (u * v) - pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = -((2 * pointY q u + pointX q u) * (2 * pointY q v + pointX q v))) (hsep : ∀ u v : K, AddParams q u v → 2 * pointY q u + pointX q u = 0 → 2 * pointY q v + pointX q v = 0 → pointX q u ≠ pointX q v) : SymAddHyps q := symAddHyps_of_sum_prod hq0 hq hsum (symAdd_prod_of_sum_diff_forall hq0 hq hsum hdiff hsep) theorem symAddHyps_of_sum_diff_of_ne (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hsum : ∀ u v : K, AddParams q u v → (pointX q (u * v) + pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = symSumNum q (pointX q u) (pointX q v)) (hdiff : ∀ u v : K, AddParams q u v → (pointX q (u * v) - pointX q (u * v⁻¹)) * (pointX q u - pointX q v) ^ 2 = -((2 * pointY q u + pointX q u) * (2 * pointY q v + pointX q v))) (hne : ∀ u v : K, AddParams q u v → pointX q u ≠ pointX q v) : SymAddHyps q := symAddHyps_of_sum_diff hq0 hq hsum hdiff (fun u v h _ _ => hne u v h) end Forall end TateCurve