`Definitions/Def_TateCurve_TorsionParametrization.lean`

definition module

Parametrising the $p$ -torsion of the Tate curve

The standing context is a complete, nontrivially normed field K with ultrametric absolute value and characteristic zero (algebraically closed from the parametrisation section onwards), elements q,\zeta,t\in K and a natural number p; curve q is the Tate curve y^2+xy=x^3+a_4(q)x+a_6(q) and pointX q u, pointY q u are the Tate series attached to a parameter u. Two objects are defined. The abbreviation WeierstrassCurve.n_torsionGen W n is Submodule.torsionBy ℤ W.toAffine.Point n, the subgroup of affine points killed by n. For q\neq 0 with \|q\|<1, p prime, \zeta a primitive p-th root of unity and t^p=q, tateTorsionPoint q ζ t … i j is the affine point with coordinates \bigl(X(\zeta^i t^j),Y(\zeta^i t^j)\bigr) when i<p, j<p and (i,j)\neq(0,0), and the point at infinity otherwise; nonsingularity follows from \zeta^i t^j\neq 0 together with tateParam_offLattice, which says that q^n\zeta^i t^j\neq 1 for all n\in\mathbb Z in that index range. For a prime p\ge 5 over algebraically closed K, tateTorsionEquiv assembles these into a bijection \mathrm{Fin}\,p\times\mathrm{Fin}\,p\simeq (curve q).n_torsionGen p, injectivity resting on tateParam_class_eq (index pairs in range with \zeta^{i'}t^{j'}=q^k\zeta^i t^j coincide) and surjectivity on eq_zero_or_eq_tateParam_unconditional; natCard_n_torsionGen_curve records \#E_q[p]=p^2.

The accompanying theorems express additivity of the uniformisation: point_inv_eq_neg (u^{-1} gives the negative of the point of u), the dichotomies point_mul_eq_add_or_sub_of_symAddHyps and point_mul_eq_add_or_neg_of_symAddHyps_of_diff, and full additivity in generic position point_mul_eq_add_of_symAddHyps_of_diffHyp; the hypotheses are the predicate SymAddHyps q, whose fields sum and prod give the symmetric sum and product identities for X(uv), X(uv^{-1}), and DiffHyp q, the identity \bigl(X(uv)-X(uv^{-1})\bigr)\bigl(X(u)-X(v)\bigr)^2=-\psi(u)\psi(v) with \psi(u)=2Y(u)+X(u), for all admissible pairs. From these, muTranslation_of_symAddHyps_of_diffHyp and muTranslation_unconditional establish MuTranslation q ζ p: for 1\le a<p and u with u and \zeta^a u off the lattice, the point of \zeta^a u is the sum of the points of \zeta^a and of u. zeta_pow_point_eq_nsmul and tateTorsionPoint_fst_eq_nsmul identify the point of \zeta^i with i times the point of \zeta, and map_pointX_tateParam, map_pointY_tateParam show that a ring isometry \sigma of K with \sigma q=q, \sigma\zeta=\zeta^e, \sigma t=\zeta^c t carries the coordinates of the pair (i,j) to those of (ei+cj,\,j), the line j=0 being preserved (map_pointX_tateParam_toric).

Relation to Mathlib

n_torsionGen is an abbreviation for Mathlib's Submodule.torsionBy ℤ applied to Mathlib's group WeierstrassCurve.Affine.Point, whose addition law and nonsingularity predicate are used throughout; Mathlib has no Tate curve or Tate uniformisation, so the Tate series, the parametrisation and the equivalence are the project's own. The lemma addX_sub_addX_negY_mul_sq, placed in the WeierstrassCurve.Affine namespace, is the antisymmetric companion of the sum and product identities for the two addX values.

Where it is used

These results give the multiplicative description of E_q[p] for a curve with multiplicative reduction: the p-torsion has exactly p^2 points, parametrised by \zeta^i t^j, and the subgroup generated by the point of \zeta is stable under isometric automorphisms fixing q. This is what makes the mod-p representation attached to a curve with multiplicative reduction upper-triangular on inertia at such a prime, as needed in the analysis of the Frey curve.

References

J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994, Chapter V
J.-P. Serre, Abelian l-adic Representations and Elliptic Curves, Benjamin, 1968, Chapter IV

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

1,089 lines
43 declarations
used in the statements of 13 theorems and imported by 21 proofs
imports 3 definition modules, and the statements of 3 theorems

Source file: Definitions/Def_TateCurve_TorsionParametrization.lean

Imports

Theorems imported by this definition module

Imported by

no other definition module

Declarations

abbrevWeierstrassCurve.n_torsionGen
lemmaWeierstrassCurve.Affine.addX_sub_addX_negY_mul_sq
lemmaTateCurve.sub_negY_curve
lemmaTateCurve.point_some_congr
lemmaTateCurve.zpow_ne_one_of_norm_lt_one
lemmaTateCurve.zpow_left_injective_of_norm_lt_one
lemmaTateCurve.tateParam_ne_zero
lemmaTateCurve.tateParam_pow
lemmaTateCurve.tateParam_offLattice
lemmaTateCurve.tateParam_class_eq
lemmaTateCurve.point_inv_eq_neg
theoremTateCurve.point_mul_eq_add_or_sub_of_symAddHyps
lemmaTateCurve.muT_norm_eq_one_of_isPrimitiveRoot
lemmaTateCurve.offLattice_zeta_pow'
theoremTateCurve.point_mul_eq_add_or_neg_of_symAddHyps_of_diff
theoremTateCurve.point_mul_eq_add_of_symAddHyps_of_diffHyp
theoremTateCurve.zeta_pow_mul_self_point_eq_add
lemmaTateCurve.muTranslation_aux
theoremTateCurve.muTranslation_of_symAddHyps_of_diffHyp
lemmaTateCurve.zeta_pow_mod
lemmaTateCurve.offLattice_zeta_pow
lemmaTateCurve.zeta_pow_point_eq_nsmul
theoremTateCurve.muTranslation_unconditional
theoremTateCurve.nsmul_prime_eq_zero_unconditional
theoremTateCurve.eq_zpow_mul_of_pointXY_eq_unconditional
lemmaTateCurve.zeta_ne_zero
lemmaTateCurve.troot_ne_zero
defTateCurve.tateTorsionPoint
lemmaTateCurve.tateTorsionPoint_spec
lemmaTateCurve.tateTorsionPoint_zero_zero
lemmaTateCurve.tateTorsionPoint_ne_zero
lemmaTateCurve.nsmul_tateTorsionPoint
lemmaTateCurve.tateTorsionPoint_mem
lemmaTateCurve.tateTorsionPoint_injOn
defTateCurve.tateTorsionEquiv
theoremTateCurve.natCard_n_torsionGen_curve
theoremTateCurve.tateTorsionPoint_zeta_mul
theoremTateCurve.tateTorsionPoint_fst_eq_nsmul
theoremTateCurve.tateTorsionPoint_inv
lemmaTateCurve.map_tateParam
theoremTateCurve.map_pointX_tateParam
theoremTateCurve.map_pointY_tateParam
theoremTateCurve.map_pointX_tateParam_toric

Source

import Mathlib
import Definitions.Def_TateCurve_XMultDistinctRouteB
import Definitions.Def_TateCurve_TateFiltrationPrep
import Definitions.Def_TateCurve_KeystoneVocab
import Theorems.Thm_TateCurve_symAddHyps_unconditional
import Theorems.Thm_TateCurve_diffHyp_unconditional
import Theorems.Thm_TateCurve_eq_zero_or_eq_tateParam_unconditional

set_option linter.unusedSectionVars false
set_option autoImplicit false

universe u

namespace WeierstrassCurve
variable {F : Type u} [Field F] [DecidableEq F] (W : WeierstrassCurve F)

abbrev n_torsionGen (n : ℕ) : Type u := Submodule.torsionBy ℤ W.toAffine.Point n
end WeierstrassCurve

namespace WeierstrassCurve.Affine
variable {F : Type*} [Field F] [DecidableEq F] {W : WeierstrassCurve F}

lemma addX_sub_addX_negY_mul_sq {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
    (W.toAffine.addX x₁ x₂ (W.toAffine.slope x₁ x₂ y₁ y₂) -
        W.toAffine.addX x₁ x₂ (W.toAffine.slope x₁ x₂ y₁ (W.toAffine.negY x₂ y₂))) *
        (x₁ - x₂) ^ 2 =
      -((y₁ - W.toAffine.negY x₁ y₁) * (y₂ - W.toAffine.negY x₂ y₂)) := by
  have e₁ := addX_mul_sq_of_X_ne (W := W.toAffine) y₁ y₂ hx
  have e₂ := addX_mul_sq_of_X_ne (W := W.toAffine) y₁ (W.toAffine.negY x₂ y₂) hx
  rw [sub_mul, e₁, e₂]
  simp only [negY]
  ring

end WeierstrassCurve.Affine

open WeierstrassCurve.Affine

namespace TateCurve

variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] [DecidableEq K]
variable {q u v w ζ t : K} {p : ℕ}

lemma sub_negY_curve (q x y : K) : y - (curve q).toAffine.negY x y = 2 * y + x := by
  rw [negY]
  show y - (-y - (curve q).a₁ * x - (curve q).a₃) = 2 * y + x
  rw [curve_a₁, curve_a₃]
  ring

private lemma point_some_congr {W : WeierstrassCurve K} {x x' y y' : K}
    (hx : x = x') (hy : y = y')
    (h : W.toAffine.Nonsingular x y) (h' : W.toAffine.Nonsingular x' y') :
    (Point.some x y h : W.toAffine.Point) = Point.some x' y' h' := by
  subst hx; subst hy; rfl

section LatticeHelpers

private lemma zpow_ne_one_of_norm_lt_one (hq : ‖q‖₊ < 1) {m : ℤ} (hm : m ≠ 0) :
    q ^ m ≠ 1 := by

  have hpos : ∀ n : ℕ, n ≠ 0 → q ^ n ≠ 1 := by
    intro n hn hcontra
    have h1 : ‖q ^ n‖₊ = 1 := by rw [hcontra, nnnorm_one]
    have h2 : ‖q ^ n‖₊ < 1 := by
      rw [nnnorm_pow]
      exact pow_lt_one₀ zero_le hq hn
    exact absurd h1 (ne_of_lt h2)
  intro hcontra
  rcases lt_trichotomy m 0 with hneg | hzero | hpos'
  ·
    have h1 : q ^ (-m) = 1 := by
      have h2 : (q ^ m)⁻¹ = (1 : K)⁻¹ := by rw [hcontra]
      rwa [← zpow_neg, inv_one] at h2
    have h2 : q ^ ((-m).toNat) = 1 := by
      rw [← zpow_natCast, Int.toNat_of_nonneg (by omega)]
      exact h1
    exact hpos (-m).toNat (by omega) h2
  · exact hm hzero
  · have h2 : q ^ (m.toNat) = 1 := by
      rw [← zpow_natCast, Int.toNat_of_nonneg (by omega)]
      exact hcontra
    exact hpos m.toNat (by omega) h2

private lemma zpow_left_injective_of_norm_lt_one (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) {m n : ℤ}
    (h : q ^ m = q ^ n) : m = n := by
  by_contra hmn
  apply zpow_ne_one_of_norm_lt_one hq (sub_ne_zero.mpr hmn)
  rw [sub_eq_add_neg, zpow_add₀ hq0, h, ← zpow_add₀ hq0, add_neg_cancel, zpow_zero]

end LatticeHelpers

section TateParameters

variable {p : ℕ}

lemma tateParam_ne_zero (hζ0 : ζ ≠ 0) (ht0 : t ≠ 0) {i j : ℕ} : ζ ^ i * t ^ j ≠ 0 :=
  mul_ne_zero (pow_ne_zero i hζ0) (pow_ne_zero j ht0)

lemma tateParam_pow (hζp : ζ ^ p = 1) (ht : t ^ p = q) (i j : ℕ) :
    (ζ ^ i * t ^ j) ^ p = q ^ (j : ℤ) := by
  have h1 : (ζ ^ i) ^ p = 1 := by rw [← pow_mul, mul_comm, pow_mul, hζp, one_pow]
  have h2 : (t ^ j) ^ p = q ^ j := by rw [← pow_mul, mul_comm, pow_mul, ht]
  rw [mul_pow, h1, h2, one_mul, zpow_natCast]

lemma tateParam_offLattice (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j : ℕ} (hi : i < p) (hj : j < p) (hij : ¬(i = 0 ∧ j = 0)) :
    OffLattice q (ζ ^ i * t ^ j) := by
  have hζp : ζ ^ p = 1 := hζ.pow_eq_one
  intro n hn

  have h1 : q ^ (n * (p : ℤ) + (j : ℤ)) = 1 := by
    have h2 : (q ^ n * (ζ ^ i * t ^ j)) ^ p = 1 := by rw [hn, one_pow]
    rwa [mul_pow, tateParam_pow hζp ht, ← zpow_natCast (q ^ n) p, ← zpow_mul,
      ← zpow_add₀ hq0] at h2

  have h3 : n * (p : ℤ) + (j : ℤ) = 0 := by
    by_contra h
    exact zpow_ne_one_of_norm_lt_one hq h h1

  have hn0 : n = 0 := by
    rcases lt_trichotomy n 0 with hneg | h0 | hpos
    · exfalso
      have hle : n * (p : ℤ) ≤ (-1) * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
    · exact h0
    · exfalso
      have hle : 1 * (p : ℤ) ≤ n * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
  have hj0 : j = 0 := by
    have h4 : (j : ℤ) = 0 := by
      rw [hn0] at h3
      simpa using h3
    exact_mod_cast h4

  have hi0 : i ≠ 0 := fun h => hij ⟨h, hj0⟩
  have h5 : ζ ^ i = 1 := by
    have h6 := hn
    rw [hn0, zpow_zero, one_mul, hj0, pow_zero, mul_one] at h6
    exact h6
  exact hi0 (hζ.pow_inj hi (by omega) (by rw [h5, pow_zero]))

lemma tateParam_class_eq (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (ht0 : t ≠ 0)
    {i j i' j' : ℕ} (hi : i < p) (hj : j < p) (hi' : i' < p) (hj' : j' < p)
    {k : ℤ} (hk : ζ ^ i' * t ^ j' = q ^ k * (ζ ^ i * t ^ j)) : i = i' ∧ j = j' := by
  have hζp : ζ ^ p = 1 := hζ.pow_eq_one

  have hpow : (q : K) ^ (j' : ℤ) = q ^ (k * (p : ℤ) + (j : ℤ)) := by
    have h1 : (ζ ^ i' * t ^ j') ^ p = (q ^ k * (ζ ^ i * t ^ j)) ^ p := by rw [hk]
    rwa [tateParam_pow hζp ht, mul_pow, tateParam_pow hζp ht, ← zpow_natCast (q ^ k) p,
      ← zpow_mul, ← zpow_add₀ hq0] at h1
  have hjj : (j' : ℤ) = k * (p : ℤ) + (j : ℤ) :=
    zpow_left_injective_of_norm_lt_one hq0 hq hpow

  have hk0 : k = 0 := by
    rcases lt_trichotomy k 0 with hneg | h0 | hpos
    · exfalso
      have hle : k * (p : ℤ) ≤ (-1) * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
    · exact h0
    · exfalso
      have hle : 1 * (p : ℤ) ≤ k * (p : ℤ) :=
        mul_le_mul_of_nonneg_right (by omega) (by positivity)
      omega
  have hjeq : j = j' := by
    have h4 : (j' : ℤ) = (j : ℤ) := by rw [hjj, hk0]; ring
    exact_mod_cast h4.symm

  have hieq : i = i' := by
    have h2 : ζ ^ i' * t ^ j = ζ ^ i * t ^ j := by
      have h3 := hk
      rw [hk0, zpow_zero, one_mul, ← hjeq] at h3
      exact h3
    have h4 : ζ ^ i' = ζ ^ i := mul_right_cancel₀ (pow_ne_zero j ht0) h2
    exact hζ.pow_inj hi hi' h4.symm
  exact ⟨hieq, hjeq⟩

end TateParameters

lemma point_inv_eq_neg (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hu0 : u ≠ 0) (hu : OffLattice q u)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q u⁻¹) (pointY q u⁻¹))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q u⁻¹) (pointY q u⁻¹) h₁ : (curve q).toAffine.Point)
      = -Point.some (pointX q u) (pointY q u) h₂ := by
  rw [Point.neg_some]
  refine point_some_congr (pointX_inv hq0 hu0 hu) ?_ h₁ _
  rw [pointY_inv hq0 hq hu0 hu, negY]
  show -pointY q u - pointX q u = -pointY q u - (curve q).a₁ * pointX q u - (curve q).a₃
  rw [curve_a₁, curve_a₃]
  ring

theorem point_mul_eq_add_or_sub_of_symAddHyps (hyps : SymAddHyps q)
    (hp : AddParams q v w) (hxne : pointX q v ≠ pointX q w)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (v * w)) (pointY q (v * w)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q v) (pointY q v))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q w) (pointY q w)) :
    (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃ ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = -(Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃) ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = Point.some (pointX q v) (pointY q v) h₂ - Point.some (pointX q w) (pointY q w) h₃ ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = -(Point.some (pointX q v) (pointY q v) h₂ - Point.some (pointX q w) (pointY q w) h₃) := by
  have hd2 : (pointX q v - pointX q w) ^ 2 ≠ 0 := pow_ne_zero 2 (sub_ne_zero.mpr hxne)

  have hS1 := hyps.sum v w hp
  have hS2 := hyps.prod v w hp
  rw [symSumNum_eq_b] at hS1
  rw [symProdNum_eq_b] at hS2

  have hsum := WeierstrassCurve.Affine.addX_add_addX_negY_mul_sq' (W := curve q)
    h₂.left h₃.left hxne
  have hprod := WeierstrassCurve.Affine.addX_mul_addX_negY_mul_sq (W := (curve q).toAffine)
    h₂.left h₃.left hxne

  have hsumEq : pointX q (v * w) + pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) +
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hS1.trans hsum.symm)
  have hprodEq : pointX q (v * w) * pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) *
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hS2.trans hprod.symm)

  have hroot : (pointX q (v * w) -
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w))) *
      (pointX q (v * w) -
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w)))) = 0 := by
    linear_combination pointX q (v * w) * hsumEq - hprodEq
  have hcond : ¬(pointX q v = pointX q w ∧
      pointY q v = (curve q).toAffine.negY (pointX q w) (pointY q w)) :=
    fun hxy => hxne hxy.left
  have hcond' : ¬(pointX q v = pointX q w ∧
      pointY q v = (curve q).toAffine.negY (pointX q w)
        ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    fun hxy => hxne hxy.left
  rcases mul_eq_zero.mp hroot with hcase | hcase
  ·
    have hxeq := sub_eq_zero.mp hcase
    have hns : (curve q).toAffine.Nonsingular
        ((curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)))
        ((curve q).toAffine.addY (pointX q v) (pointX q w) (pointY q v)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w))) :=
      WeierstrassCurve.Affine.nonsingular_add h₂ h₃ hcond
    rcases WeierstrassCurve.Affine.Y_eq_of_X_eq h₁.left hns.left hxeq with hyeq | hyeq
    · left
      rw [Point.add_of_X_ne hxne]
      exact point_some_congr hxeq hyeq h₁ _
    · right; left
      rw [Point.add_of_X_ne hxne, Point.neg_some]
      exact point_some_congr hxeq hyeq h₁ _
  ·
    have hxeq := sub_eq_zero.mp hcase
    have hns : (curve q).toAffine.Nonsingular
        ((curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))))
        ((curve q).toAffine.addY (pointX q v) (pointX q w) (pointY q v)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w)))) :=
      WeierstrassCurve.Affine.nonsingular_add h₂ ((nonsingular_neg _ _).mpr h₃) hcond'
    rcases WeierstrassCurve.Affine.Y_eq_of_X_eq h₁.left hns.left hxeq with hyeq | hyeq
    · right; right; left
      rw [sub_eq_add_neg, Point.neg_some, Point.add_of_X_ne hxne]
      exact point_some_congr hxeq hyeq h₁ _
    · right; right; right
      rw [sub_eq_add_neg, Point.neg_some, Point.add_of_X_ne hxne, Point.neg_some]
      exact point_some_congr hxeq hyeq h₁ _

private lemma muT_norm_eq_one_of_isPrimitiveRoot (hζ : IsPrimitiveRoot ζ p) (hp0 : p ≠ 0) :
    ‖ζ‖ = 1 := by
  have h1 : ‖ζ‖ ^ p = 1 := by rw [← norm_pow, hζ.pow_eq_one, norm_one]
  rcases (pow_eq_one_iff_of_ne_zero hp0).mp h1 with h | ⟨h, _⟩
  · exact h
  · exfalso
    have h2 := norm_nonneg ζ
    rw [h] at h2
    linarith

private lemma offLattice_zeta_pow' (hq0 : q ≠ 0) (hq1 : ‖q‖ < 1) (hζ : IsPrimitiveRoot ζ p)
    (hp0 : p ≠ 0) {k : ℕ} (hk : ¬ p ∣ k) : OffLattice q (ζ ^ k) :=
  offLattice_of_norm_eq_one hq0 hq1
    (by rw [norm_pow, muT_norm_eq_one_of_isPrimitiveRoot hζ hp0, one_pow])
    (fun h1 => hk ((hζ.pow_eq_one_iff_dvd k).mp h1))

theorem point_mul_eq_add_or_neg_of_symAddHyps_of_diff (hyps : SymAddHyps q)
    (hd1 : (pointX q (v * w) - pointX q (v * w⁻¹)) * (pointX q v - pointX q w) ^ 2 =
      -((2 * pointY q v + pointX q v) * (2 * pointY q w + pointX q w)))
    (hp : AddParams q v w) (hxne : pointX q v ≠ pointX q w)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (v * w)) (pointY q (v * w)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q v) (pointY q v))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q w) (pointY q w)) :
    (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃ ∨
      (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
        = -(Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃) := by
  have hd2 : (pointX q v - pointX q w) ^ 2 ≠ 0 := pow_ne_zero 2 (sub_ne_zero.mpr hxne)

  have hS1 := hyps.sum v w hp
  rw [symSumNum_eq_b] at hS1
  have hsum := WeierstrassCurve.Affine.addX_add_addX_negY_mul_sq' (W := curve q)
    h₂.left h₃.left hxne
  have hsumEq : pointX q (v * w) + pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) +
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hS1.trans hsum.symm)

  have hdiffC := WeierstrassCurve.Affine.addX_sub_addX_negY_mul_sq (W := curve q)
    (pointY q v) (pointY q w) hxne
  rw [sub_negY_curve, sub_negY_curve] at hdiffC
  have hdiffEq : pointX q (v * w) - pointX q (v * w⁻¹) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) -
        (curve q).toAffine.addX (pointX q v) (pointX q w)
          ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v)
            ((curve q).toAffine.negY (pointX q w) (pointY q w))) :=
    mul_right_cancel₀ hd2 (hd1.trans hdiffC.symm)

  have hxeq : pointX q (v * w) =
      (curve q).toAffine.addX (pointX q v) (pointX q w)
        ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)) := by
    have h2 : (2 : K) ≠ 0 := by norm_num
    apply mul_left_cancel₀ h2
    linear_combination hsumEq + hdiffEq

  have hcond : ¬(pointX q v = pointX q w ∧
      pointY q v = (curve q).toAffine.negY (pointX q w) (pointY q w)) :=
    fun hxy => hxne hxy.left
  have hns : (curve q).toAffine.Nonsingular
      ((curve q).toAffine.addX (pointX q v) (pointX q w)
        ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w)))
      ((curve q).toAffine.addY (pointX q v) (pointX q w) (pointY q v)
        ((curve q).toAffine.slope (pointX q v) (pointX q w) (pointY q v) (pointY q w))) :=
    WeierstrassCurve.Affine.nonsingular_add h₂ h₃ hcond
  rcases WeierstrassCurve.Affine.Y_eq_of_X_eq h₁.left hns.left hxeq with hyeq | hyeq
  · left
    rw [Point.add_of_X_ne hxne]
    exact point_some_congr hxeq hyeq h₁ _
  · right
    rw [Point.add_of_X_ne hxne, Point.neg_some]
    exact point_some_congr hxeq hyeq h₁ _

theorem point_mul_eq_add_of_symAddHyps_of_diffHyp (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hp : AddParams q v w) (hxne : pointX q v ≠ pointX q w)
    (hp' : AddParams q (v * w) v⁻¹) (hxne' : pointX q (v * w) ≠ pointX q v)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (v * w)) (pointY q (v * w)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q v) (pointY q v))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q w) (pointY q w))
    (hP2 : (Point.some (pointX q v) (pointY q v) h₂ : (curve q).toAffine.Point)
        + Point.some (pointX q v) (pointY q v) h₂ ≠ 0) :
    (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
      = Point.some (pointX q v) (pointY q v) h₂ + Point.some (pointX q w) (pointY q w) h₃ := by

  have hvw0 : v * w ≠ 0 := mul_ne_zero hp.u_ne_zero hp.v_ne_zero
  have hprod0 : (v * w) * v⁻¹ ≠ 0 := mul_ne_zero hvw0 (inv_ne_zero hp.u_ne_zero)
  have h₄ : (curve q).toAffine.Nonsingular (pointX q ((v * w) * v⁻¹)) (pointY q ((v * w) * v⁻¹)) :=
    nonsingular_point hq0 hq hprod0 hp'.offLattice_mul
  have hinv0 : v⁻¹ ≠ 0 := inv_ne_zero hp.u_ne_zero
  have hinvOff : OffLattice q v⁻¹ := OffLattice.inv hq0 hp.offLattice_u
  have h₅ : (curve q).toAffine.Nonsingular (pointX q v⁻¹) (pointY q v⁻¹) :=
    nonsingular_point hq0 hq hinv0 hinvOff

  set R := (Point.some (pointX q (v * w)) (pointY q (v * w)) h₁ : (curve q).toAffine.Point)
    with hR_def
  set P := (Point.some (pointX q v) (pointY q v) h₂ : (curve q).toAffine.Point) with hP_def
  set Q := (Point.some (pointX q w) (pointY q w) h₃ : (curve q).toAffine.Point) with hQ_def

  have hxneDer : pointX q (v * w) ≠ pointX q v⁻¹ := by
    rw [pointX_inv hq0 hp.u_ne_zero hp.offLattice_u]
    exact hxne'
  have hder := point_mul_eq_add_or_neg_of_symAddHyps_of_diff hyps
    (hdiff (v * w) v⁻¹ hp') hp' hxneDer h₄ h₁ h₅

  have helem : (v * w) * v⁻¹ = w := by
    rw [mul_comm v w, mul_assoc, mul_inv_cancel₀ hp.u_ne_zero, mul_one]
  have e₄ : (Point.some (pointX q ((v * w) * v⁻¹)) (pointY q ((v * w) * v⁻¹)) h₄ :
      (curve q).toAffine.Point) = Q :=
    point_some_congr (congrArg (pointX q) helem) (congrArg (pointY q) helem) h₄ h₃
  have e₅ : (Point.some (pointX q v⁻¹) (pointY q v⁻¹) h₅ : (curve q).toAffine.Point) = -P :=
    point_inv_eq_neg hq0 hq hp.u_ne_zero hp.offLattice_u h₅ h₂
  rw [e₄, e₅] at hder

  rcases hder with hder | hder
  ·
    calc R = P + (R + -P) := by abel
      _ = P + Q := by rw [← hder]
  ·
    rcases point_mul_eq_add_or_neg_of_symAddHyps_of_diff hyps (hdiff v w hp) hp hxne h₁ h₂ h₃
      with hmain | hmain
    · exact hmain
    ·
      exfalso
      apply hP2
      have k1 : R + (P + Q) = 0 := by rw [hR_def, hmain]; abel
      have k2 : Q + (R + -P) = 0 := by rw [hder]; abel
      calc P + P = (R + (P + Q)) - (Q + (R + -P)) := by abel
        _ = 0 - 0 := by rw [k1, k2]
        _ = 0 := by abel

theorem zeta_pow_mul_self_point_eq_add (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p) (hpp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a))) :
    (Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) h₁ :
        (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂
          + Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ := by

  have hp0 : p ≠ 0 := by omega
  have hζ0 : ζ ≠ 0 := hζ.ne_zero hp0
  have hζa0 : ζ ^ a ≠ 0 := pow_ne_zero _ hζ0
  have hq1 : ‖q‖ < 1 := by exact_mod_cast hq
  have hnζ : ‖ζ‖ = 1 := muT_norm_eq_one_of_isPrimitiveRoot hζ hp0
  have hnζa : ‖ζ ^ a‖ = 1 := by rw [norm_pow, hnζ, one_pow]
  have hndvd_a : ¬ p ∣ a := fun hdvd =>
    absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)
  have hndvd_2a : ¬ p ∣ a + a := by
    intro hdvd
    rw [← two_mul a] at hdvd
    rcases (Nat.Prime.dvd_mul hpp).mp hdvd with h2 | ha
    · exact absurd (Nat.le_of_dvd (by norm_num) h2) (by omega)
    · exact hndvd_a ha
  have hndvd_3a : ¬ p ∣ a + a + a := by
    intro hdvd
    have h3a : a + a + a = 3 * a := by ring
    rw [h3a] at hdvd
    rcases (Nat.Prime.dvd_mul hpp).mp hdvd with h3 | ha
    · exact absurd (Nat.le_of_dvd (by norm_num) h3) (by omega)
    · exact hndvd_a ha
  have hndvd_pa : ¬ p ∣ p - a := fun hdvd =>
    absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)

  have hζaOff : OffLattice q (ζ ^ a) := offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_a
  have hζ2aOff : OffLattice q (ζ ^ a * ζ ^ a) := by
    rw [← pow_add]
    exact offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_2a
  have hζpaOff : OffLattice q (ζ ^ (p - a)) := offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_pa

  have hpa_inv : ζ ^ (p - a) = (ζ ^ a)⁻¹ := by
    have hcancel : ζ ^ a * ζ ^ (p - a) = ζ ^ a * (ζ ^ a)⁻¹ := by
      rw [mul_inv_cancel₀ hζa0, ← pow_add, show a + (p - a) = p by omega, hζ.pow_eq_one]
    exact mul_left_cancel₀ hζa0 hcancel

  have helem1 : (ζ ^ a * ζ ^ a) * ζ ^ (p - a) = ζ ^ a := by
    rw [mul_assoc, ← pow_add, show a + (p - a) = p by omega, hζ.pow_eq_one, mul_one]

  have hpDouble : AddParams q (ζ ^ a * ζ ^ a) (ζ ^ (p - a)) := by
    refine ⟨hq0, mul_ne_zero hζa0 hζa0, pow_ne_zero _ hζ0, hζ2aOff, hζpaOff, ?_, ?_⟩
    · rw [helem1]; exact hζaOff
    · have helem2 : (ζ ^ a * ζ ^ a) * (ζ ^ (p - a))⁻¹ = ζ ^ (a + a + a) := by
        rw [hpa_inv, inv_inv, ← pow_add, ← pow_add]
      rw [helem2]
      exact offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_3a

  have hxneDouble : pointX q (ζ ^ a * ζ ^ a) ≠ pointX q (ζ ^ (p - a)) := by
    intro hX
    rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq (mul_ne_zero hζa0 hζa0) (pow_ne_zero _ hζ0)
      hζ2aOff hζpaOff
      (le_of_eq (by rw [norm_mul, hnζa, one_mul]))
      (le_of_eq (by rw [norm_pow, hnζ, one_pow]))
      (by rw [helem1, hnζa]; exact hq1) hX with heq | hone
    ·
      apply hndvd_3a
      have h1 : ζ ^ (a + a + a) = 1 := by
        rw [pow_add, pow_add, heq, ← pow_add, show p - a + a = p by omega, hζ.pow_eq_one]
      exact (hζ.pow_eq_one_iff_dvd _).mp h1
    ·
      rw [helem1] at hone
      exact hndvd_a ((hζ.pow_eq_one_iff_dvd a).mp hone)

  have hprodNs : (curve q).toAffine.Nonsingular (pointX q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a)))
      (pointY q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a))) :=
    nonsingular_point hq0 hq (mul_ne_zero (mul_ne_zero hζa0 hζa0) (pow_ne_zero _ hζ0))
      hpDouble.offLattice_mul
  have hwNs : (curve q).toAffine.Nonsingular (pointX q (ζ ^ (p - a))) (pointY q (ζ ^ (p - a))) :=
    nonsingular_point hq0 hq (pow_ne_zero _ hζ0) hζpaOff

  have hcase := point_mul_eq_add_or_neg_of_symAddHyps_of_diff hyps
    (hdiff (ζ ^ a * ζ ^ a) (ζ ^ (p - a)) hpDouble) hpDouble hxneDouble hprodNs h₁ hwNs

  have e1 : (Point.some (pointX q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a)))
      (pointY q ((ζ ^ a * ζ ^ a) * ζ ^ (p - a))) hprodNs : (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :=
    point_some_congr (congrArg (pointX q) helem1) (congrArg (pointY q) helem1) hprodNs h₂
  have hwNs' : (curve q).toAffine.Nonsingular (pointX q ((ζ ^ a)⁻¹)) (pointY q ((ζ ^ a)⁻¹)) := by
    rw [← hpa_inv]
    exact hwNs
  have e2 : (Point.some (pointX q (ζ ^ (p - a))) (pointY q (ζ ^ (p - a))) hwNs :
      (curve q).toAffine.Point)
      = -(Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂) := by
    have e2' : (Point.some (pointX q (ζ ^ (p - a))) (pointY q (ζ ^ (p - a))) hwNs :
        (curve q).toAffine.Point)
        = Point.some (pointX q ((ζ ^ a)⁻¹)) (pointY q ((ζ ^ a)⁻¹)) hwNs' :=
      point_some_congr (congrArg (pointX q) hpa_inv) (congrArg (pointY q) hpa_inv) hwNs hwNs'
    rw [e2']
    exact point_inv_eq_neg hq0 hq hζa0 hζaOff hwNs' h₂
  rw [e1, e2] at hcase

  set P2 := (Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) h₁ :
    (curve q).toAffine.Point) with hP2_def
  set P1 := (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
    (curve q).toAffine.Point) with hP1_def
  rcases hcase with hc | hc
  ·
    calc P2 = (P2 + -P1) + P1 := by abel
      _ = P1 + P1 := by rw [← hc]
  ·
    exfalso
    have k : P1 + (P2 + -P1) = 0 := by
      nth_rewrite 1 [hc]
      abel
    have h0 : P2 = 0 := by
      calc P2 = P1 + (P2 + -P1) := by abel
        _ = 0 := k
    exact Point.some_ne_zero h₁ h0

private lemma muTranslation_aux (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p) (hpp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u) (hau : OffLattice q (ζ ^ a * u))
    (hule : ‖u‖ ≤ 1) (hqlt : ‖q‖ < ‖u‖)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a)))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ : (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂
          + Point.some (pointX q u) (pointY q u) h₃ := by

  have hp0 : p ≠ 0 := by omega
  have hζ0 : ζ ≠ 0 := hζ.ne_zero hp0
  have hζa0 : ζ ^ a ≠ 0 := pow_ne_zero _ hζ0
  have hq1 : ‖q‖ < 1 := by exact_mod_cast hq
  have hnζ : ‖ζ‖ = 1 := muT_norm_eq_one_of_isPrimitiveRoot hζ hp0
  have hnζa : ‖ζ ^ a‖ = 1 := by rw [norm_pow, hnζ, one_pow]
  have hndvd_a : ¬ p ∣ a := fun hdvd =>
    absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)
  have hndvd_2a : ¬ p ∣ a + a := by
    intro hdvd
    rw [← two_mul a] at hdvd
    rcases (Nat.Prime.dvd_mul hpp).mp hdvd with h2 | ha
    · exact absurd (Nat.le_of_dvd (by norm_num) h2) (by omega)
    · exact hndvd_a ha
  have hζaOff : OffLattice q (ζ ^ a) := offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_a
  have hζ2aOff : OffLattice q (ζ ^ a * ζ ^ a) := by
    rw [← pow_add]
    exact offLattice_zeta_pow' hq0 hq1 hζ hp0 hndvd_2a

  have hDns : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * ζ ^ a))
      (pointY q (ζ ^ a * ζ ^ a)) :=
    nonsingular_point hq0 hq (mul_ne_zero hζa0 hζa0) hζ2aOff

  by_cases hC2 : OffLattice q (ζ ^ a * u⁻¹)
  · by_cases hC4 : OffLattice q (ζ ^ a * ζ ^ a * u)
    ·
      have hpMain : AddParams q (ζ ^ a) u := ⟨hq0, hζa0, hu0, hζaOff, hu, hau, hC2⟩
      have hxneMain : pointX q (ζ ^ a) ≠ pointX q u := by
        intro hX
        rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq hζa0 hu0 hζaOff hu (le_of_eq hnζa) hule
          (by rw [norm_mul, hnζa, one_mul]; exact hqlt) hX with heq | hone
        ·
          apply hC2 0
          rw [zpow_zero, one_mul, heq, mul_inv_cancel₀ hu0]
        ·
          exact hau 0 (by rw [zpow_zero, one_mul]; exact hone)
      have hpDer : AddParams q (ζ ^ a * u) (ζ ^ a)⁻¹ := by
        refine ⟨hq0, mul_ne_zero hζa0 hu0, inv_ne_zero hζa0, hau,
          OffLattice.inv hq0 hζaOff, ?_, ?_⟩
        · have helem : (ζ ^ a * u) * (ζ ^ a)⁻¹ = u := by
            rw [mul_comm (ζ ^ a) u, mul_assoc, mul_inv_cancel₀ hζa0, mul_one]
          rw [helem]; exact hu
        · have helem : (ζ ^ a * u) * ((ζ ^ a)⁻¹)⁻¹ = ζ ^ a * ζ ^ a * u := by
            rw [inv_inv]; ring
          rw [helem]; exact hC4
      have hxneDer : pointX q (ζ ^ a * u) ≠ pointX q (ζ ^ a) := by
        intro hX
        rcases eq_or_mul_eq_one_of_pointX_eq hq0 hq (mul_ne_zero hζa0 hu0) hζa0 hau hζaOff
          (by rw [norm_mul, hnζa, one_mul]; exact hule) (le_of_eq hnζa)
          (by rw [norm_mul, norm_mul, hnζa, one_mul, mul_one]; exact hqlt) hX with heq | hone
        ·
          have hu1 : u = 1 := by
            have h := heq.trans (mul_one (ζ ^ a)).symm
            exact mul_left_cancel₀ hζa0 h
          exact hu 0 (by rw [zpow_zero, one_mul, hu1])
        ·
          apply hC4 0
          rw [zpow_zero, one_mul]
          calc ζ ^ a * ζ ^ a * u = (ζ ^ a * u) * ζ ^ a := by ring
            _ = 1 := hone

      have hP2 : (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
          (curve q).toAffine.Point)
          + Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ ≠ 0 := by
        intro h2tor
        have hodd : Odd p := hpp.odd_of_ne_two (by omega)
        have hpow : (ζ ^ a) ^ p = q ^ (0 : ℤ) := by
          rw [← pow_mul, mul_comm a p, pow_mul, hζ.pow_eq_one, one_pow, zpow_zero]
        have hptor : p • (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
            (curve q).toAffine.Point) = 0 :=
          nsmul_prime_eq_zero hyps hq0 hq hζa0 hζaOff hpow hpp hodd h₂
        set PT := (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :
          (curve q).toAffine.Point) with hPT_def
        obtain ⟨k, hk⟩ := hodd
        have hk' : p = k + k + 1 := by omega
        have hpP : p • PT = PT := by
          calc p • PT = (k + k + 1) • PT := by rw [← hk']
            _ = k • PT + k • PT + PT := by rw [add_nsmul, add_nsmul, one_nsmul]
            _ = k • (PT + PT) + PT := by rw [← nsmul_add]
            _ = PT := by rw [h2tor, smul_zero, zero_add]
        have h0 : PT = 0 := by rw [← hpP, hptor]
        exact Point.some_ne_zero h₂ h0
      exact point_mul_eq_add_of_symAddHyps_of_diffHyp hyps hdiff hq0 hq hpMain hxneMain hpDer
        hxneDer h₁ h₂ h₃ hP2
    ·
      have hdouble := zeta_pow_mul_self_point_eq_add hyps hdiff hq0 hq hp5 hpp hζ ha1 hap hDns h₂
      have hC4' : ∃ n : ℤ, q ^ n * (ζ ^ a * ζ ^ a * u) = 1 := by
        by_contra hcon
        exact hC4 (fun n hn => hcon ⟨n, hn⟩)
      obtain ⟨n, hn⟩ := hC4'

      have hqn0 : (q : K) ^ n ≠ 0 := zpow_ne_zero _ hq0
      have hzu_eq : ζ ^ a * u = q ^ (-n) * (ζ ^ a)⁻¹ := by
        have hcancel : (q ^ n * ζ ^ a) * (ζ ^ a * u) =
            (q ^ n * ζ ^ a) * (q ^ (-n) * (ζ ^ a)⁻¹) := by
          rw [show (q ^ n * ζ ^ a) * (ζ ^ a * u) = q ^ n * (ζ ^ a * ζ ^ a * u) by ring, hn,
            show (q ^ n * ζ ^ a) * (q ^ (-n) * (ζ ^ a)⁻¹) =
              (q ^ n * q ^ (-n)) * (ζ ^ a * (ζ ^ a)⁻¹) by ring,
            ← zpow_add₀ hq0, show n + -n = 0 by omega, zpow_zero,
            mul_inv_cancel₀ hζa0, mul_one]
        exact mul_left_cancel₀ (mul_ne_zero hqn0 hζa0) hcancel
      have hu_eq : u = q ^ (-n) * (ζ ^ a * ζ ^ a)⁻¹ := by
        have hcancel : (q ^ n * (ζ ^ a * ζ ^ a)) * u =
            (q ^ n * (ζ ^ a * ζ ^ a)) * (q ^ (-n) * (ζ ^ a * ζ ^ a)⁻¹) := by
          rw [show (q ^ n * (ζ ^ a * ζ ^ a)) * u = q ^ n * (ζ ^ a * ζ ^ a * u) by ring, hn,
            show (q ^ n * (ζ ^ a * ζ ^ a)) * (q ^ (-n) * (ζ ^ a * ζ ^ a)⁻¹) =
              (q ^ n * q ^ (-n)) * ((ζ ^ a * ζ ^ a) * (ζ ^ a * ζ ^ a)⁻¹) by ring,
            ← zpow_add₀ hq0, show n + -n = 0 by omega, zpow_zero,
            mul_inv_cancel₀ (mul_ne_zero hζa0 hζa0), mul_one]
        exact mul_left_cancel₀ (mul_ne_zero hqn0 (mul_ne_zero hζa0 hζa0)) hcancel

      have hXzu : pointX q (ζ ^ a * u) = pointX q (ζ ^ a) := by
        rw [hzu_eq, pointX_zpow_mul hq0, pointX_inv hq0 hζa0 hζaOff]
      have hYzu : pointY q (ζ ^ a * u) = -pointY q (ζ ^ a) - pointX q (ζ ^ a) := by
        rw [hzu_eq, pointY_zpow_mul hq0, pointY_inv hq0 hq hζa0 hζaOff]
      have hXu : pointX q u = pointX q (ζ ^ a * ζ ^ a) := by
        rw [hu_eq, pointX_zpow_mul hq0, pointX_inv hq0 (mul_ne_zero hζa0 hζa0) hζ2aOff]
      have hYu : pointY q u = -pointY q (ζ ^ a * ζ ^ a) - pointX q (ζ ^ a * ζ ^ a) := by
        rw [hu_eq, pointY_zpow_mul hq0, pointY_inv hq0 hq (mul_ne_zero hζa0 hζa0) hζ2aOff]

      have hL : (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
          (curve q).toAffine.Point)
          = -(Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂) := by
        rw [Point.neg_some]
        refine point_some_congr hXzu ?_ h₁ _
        rw [hYzu, negY]
        show -pointY q (ζ ^ a) - pointX q (ζ ^ a) =
          -pointY q (ζ ^ a) - (curve q).a₁ * pointX q (ζ ^ a) - (curve q).a₃
        rw [curve_a₁, curve_a₃]
        ring
      have hU : (Point.some (pointX q u) (pointY q u) h₃ : (curve q).toAffine.Point)
          = -(Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) hDns) := by
        rw [Point.neg_some]
        refine point_some_congr hXu ?_ h₃ _
        rw [hYu, negY]
        show -pointY q (ζ ^ a * ζ ^ a) - pointX q (ζ ^ a * ζ ^ a) =
          -pointY q (ζ ^ a * ζ ^ a) - (curve q).a₁ * pointX q (ζ ^ a * ζ ^ a) - (curve q).a₃
        rw [curve_a₁, curve_a₃]
        ring
      rw [hL, hU, hdouble]
      abel
  ·

    have hdouble := zeta_pow_mul_self_point_eq_add hyps hdiff hq0 hq hp5 hpp hζ ha1 hap hDns h₂
    have hC2' : ∃ n : ℤ, q ^ n * (ζ ^ a * u⁻¹) = 1 := by
      by_contra hcon
      exact hC2 (fun n hn => hcon ⟨n, hn⟩)
    obtain ⟨n, hn⟩ := hC2'

    have hu_eq : u = q ^ n * ζ ^ a := by
      have h1 : (q ^ n * (ζ ^ a * u⁻¹)) * u = u := by rw [hn, one_mul]
      have h2 : (q ^ n * ζ ^ a) * (u⁻¹ * u) = u := by
        calc (q ^ n * ζ ^ a) * (u⁻¹ * u) = (q ^ n * (ζ ^ a * u⁻¹)) * u := by ring
          _ = u := h1
      rw [inv_mul_cancel₀ hu0, mul_one] at h2
      exact h2.symm

    have hXu : pointX q u = pointX q (ζ ^ a) := by rw [hu_eq, pointX_zpow_mul hq0]
    have hYu : pointY q u = pointY q (ζ ^ a) := by rw [hu_eq, pointY_zpow_mul hq0]
    have hzu_eq : ζ ^ a * u = q ^ n * (ζ ^ a * ζ ^ a) := by rw [hu_eq]; ring
    have hXzu : pointX q (ζ ^ a * u) = pointX q (ζ ^ a * ζ ^ a) := by
      rw [hzu_eq, pointX_zpow_mul hq0]
    have hYzu : pointY q (ζ ^ a * u) = pointY q (ζ ^ a * ζ ^ a) := by
      rw [hzu_eq, pointY_zpow_mul hq0]
    have hL : (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
        (curve q).toAffine.Point)
        = Point.some (pointX q (ζ ^ a * ζ ^ a)) (pointY q (ζ ^ a * ζ ^ a)) hDns :=
      point_some_congr hXzu hYzu h₁ hDns
    have hU : (Point.some (pointX q u) (pointY q u) h₃ : (curve q).toAffine.Point)
        = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂ :=
      point_some_congr hXu hYu h₃ h₂
    rw [hL, hU]
    exact hdouble

theorem muTranslation_of_symAddHyps_of_diffHyp (hyps : SymAddHyps q) (hdiff : DiffHyp q)
    (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p) (hpp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) :
    MuTranslation q ζ p := by
  intro a ha1 hap u hu0 hu hau h₁ h₂ h₃

  have hq1 : ‖q‖ < 1 := by exact_mod_cast hq
  have hqpos : (0 : ℝ) < ‖q‖ := norm_pos_iff.mpr hq0
  have hupos : (0 : ℝ) < ‖u‖ := norm_pos_iff.mpr hu0
  obtain ⟨m, hm⟩ := exists_mem_Ioc_zpow (x := ‖u‖) (y := ‖q‖⁻¹) hupos
    ((one_lt_inv₀ hqpos).mpr hq1)
  have hinv_zpow : ∀ k : ℤ, (‖q‖⁻¹) ^ k = ‖q‖ ^ (-k) := by
    intro k
    rw [inv_zpow, ← zpow_neg]

  set u' := q ^ (m + 1) * u with hu'_def
  have hu'0 : u' ≠ 0 := mul_ne_zero (zpow_ne_zero _ hq0) hu0
  have hu' : OffLattice q u' := OffLattice.zpow_mul hq0 (m + 1) hu
  have hau' : OffLattice q (ζ ^ a * u') := by
    have helem : ζ ^ a * u' = q ^ (m + 1) * (ζ ^ a * u) := by rw [hu'_def]; ring
    rw [helem]
    exact OffLattice.zpow_mul hq0 (m + 1) hau

  have hnorm_u' : ‖u'‖ = ‖q‖ ^ (m + 1) * ‖u‖ := by
    rw [hu'_def, norm_mul, norm_zpow]
  have hu'le : ‖u'‖ ≤ 1 := by
    rw [hnorm_u']
    have h1 : ‖u‖ ≤ ‖q‖ ^ (-(m + 1)) := by
      have h2 := hm.2
      rwa [hinv_zpow (m + 1)] at h2
    calc ‖q‖ ^ (m + 1) * ‖u‖ ≤ ‖q‖ ^ (m + 1) * ‖q‖ ^ (-(m + 1)) :=
          mul_le_mul_of_nonneg_left h1 (le_of_lt (zpow_pos hqpos _))
      _ = 1 := by
          rw [← zpow_add₀ (ne_of_gt hqpos), show m + 1 + -(m + 1) = 0 by omega, zpow_zero]
  have hu'gt : ‖q‖ < ‖u'‖ := by
    rw [hnorm_u']
    have h1 : ‖q‖ ^ (-m) < ‖u‖ := by
      have h2 := hm.1
      rwa [hinv_zpow m] at h2
    calc ‖q‖ = ‖q‖ ^ (m + 1) * ‖q‖ ^ (-m) := by
          rw [← zpow_add₀ (ne_of_gt hqpos), show m + 1 + -m = 1 by omega, zpow_one]
      _ < ‖q‖ ^ (m + 1) * ‖u‖ := mul_lt_mul_of_pos_left h1 (zpow_pos hqpos _)

  have hXu' : pointX q u' = pointX q u := by rw [hu'_def, pointX_zpow_mul hq0]
  have hYu' : pointY q u' = pointY q u := by rw [hu'_def, pointY_zpow_mul hq0]
  have hzuelem : ζ ^ a * u' = q ^ (m + 1) * (ζ ^ a * u) := by rw [hu'_def]; ring
  have hXzu' : pointX q (ζ ^ a * u') = pointX q (ζ ^ a * u) := by
    rw [hzuelem, pointX_zpow_mul hq0]
  have hYzu' : pointY q (ζ ^ a * u') = pointY q (ζ ^ a * u) := by
    rw [hzuelem, pointY_zpow_mul hq0]

  have h₁' : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * u')) (pointY q (ζ ^ a * u')) := by
    rw [hXzu', hYzu']; exact h₁
  have h₃' : (curve q).toAffine.Nonsingular (pointX q u') (pointY q u') := by
    rw [hXu', hYu']; exact h₃

  have haux := muTranslation_aux hyps hdiff hq0 hq hp5 hpp hζ ha1 hap hu'0 hu' hau'
    hu'le hu'gt h₁' h₂ h₃'
  have e₁ : (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
      (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a * u')) (pointY q (ζ ^ a * u')) h₁' :=
    point_some_congr hXzu'.symm hYzu'.symm h₁ h₁'
  have e₃ : (Point.some (pointX q u) (pointY q u) h₃ : (curve q).toAffine.Point)
      = Point.some (pointX q u') (pointY q u') h₃' :=
    point_some_congr hXu'.symm hYu'.symm h₃ h₃'
  rw [e₁, e₃]
  exact haux

lemma zeta_pow_mod (hζp : ζ ^ p = 1) (n : ℕ) : ζ ^ n = ζ ^ (n % p) := by
  conv_lhs => rw [← Nat.mod_add_div n p]
  rw [pow_add, pow_mul, hζp, one_pow, mul_one]

lemma offLattice_zeta_pow (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hζ : IsPrimitiveRoot ζ p)
    (ht : t ^ p = q) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p) : OffLattice q (ζ ^ a) := by
  have hp0 : 0 < p := lt_of_le_of_lt (Nat.zero_le a) hap
  have h := tateParam_offLattice (t := t) hq0 hq hζ ht hap hp0 (fun h => by omega)
  rwa [pow_zero, mul_one] at h

lemma zeta_pow_point_eq_nsmul (hμ : MuTranslation q ζ p) (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    (hp : p.Prime) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (hζpt : (curve q).toAffine.Nonsingular (pointX q ζ) (pointY q ζ)) :
    ∀ a : ℕ, 1 ≤ a → a < p →
      ∀ h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a)),
        (Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₁ : (curve q).toAffine.Point)
          = a • Point.some (pointX q ζ) (pointY q ζ) hζpt := by
  have hζ0 : ζ ≠ 0 := fun h0 => by
    have hζp := hζ.pow_eq_one
    rw [h0, zero_pow hp.ne_zero] at hζp
    exact zero_ne_one hζp
  intro a
  induction a with
  | zero => intro h; omega
  | succ n ih =>
    intro _ hlt h₁
    rcases Nat.lt_or_ge n 1 with h2 | h2
    ·
      have hn0 : n = 0 := by omega
      subst hn0
      have hx : ζ ^ 1 = ζ := pow_one ζ
      rw [one_nsmul]
      exact point_some_congr (congrArg (pointX q) hx) (congrArg (pointY q) hx) h₁ hζpt
    ·
      have hnp : n < p := by omega
      have hparam : ζ ^ 1 * ζ ^ n = ζ ^ (n + 1) := by
        rw [pow_one, mul_comm, ← pow_succ]
      have hu0 : (ζ : K) ^ n ≠ 0 := pow_ne_zero _ hζ0
      have huoff : OffLattice q (ζ ^ n) := offLattice_zeta_pow hq0 hq hζ ht h2 hnp
      have hprodoff : OffLattice q (ζ ^ 1 * ζ ^ n) := by
        have h := offLattice_zeta_pow hq0 hq hζ ht (a := n + 1) (by omega) hlt
        rwa [← hparam] at h
      have h₁' : (curve q).toAffine.Nonsingular (pointX q (ζ ^ 1 * ζ ^ n))
          (pointY q (ζ ^ 1 * ζ ^ n)) := by rw [hparam]; exact h₁
      have h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ 1)) (pointY q (ζ ^ 1)) := by
        rw [pow_one]; exact hζpt
      have hns_n : (curve q).toAffine.Nonsingular (pointX q (ζ ^ n)) (pointY q (ζ ^ n)) :=
        nonsingular_point hq0 hq hu0 huoff
      have htrans := hμ 1 le_rfl (by omega) (ζ ^ n) hu0 huoff hprodoff h₁' h₂ hns_n
      calc (Point.some (pointX q (ζ ^ (n + 1))) (pointY q (ζ ^ (n + 1))) h₁ :
              (curve q).toAffine.Point)
          = Point.some (pointX q (ζ ^ 1 * ζ ^ n)) (pointY q (ζ ^ 1 * ζ ^ n)) h₁' :=
            point_some_congr (congrArg (pointX q) hparam.symm)
              (congrArg (pointY q) hparam.symm) h₁ h₁'
        _ = Point.some (pointX q (ζ ^ 1)) (pointY q (ζ ^ 1)) h₂
              + Point.some (pointX q (ζ ^ n)) (pointY q (ζ ^ n)) hns_n := htrans
        _ = Point.some (pointX q ζ) (pointY q ζ) hζpt
              + Point.some (pointX q (ζ ^ n)) (pointY q (ζ ^ n)) hns_n := by
            congr 1
            exact point_some_congr (congrArg (pointX q) (pow_one ζ))
              (congrArg (pointY q) (pow_one ζ)) h₂ hζpt
        _ = Point.some (pointX q ζ) (pointY q ζ) hζpt
              + n • Point.some (pointX q ζ) (pointY q ζ) hζpt := by
            rw [ih h2 hnp hns_n]
        _ = (n + 1) • Point.some (pointX q ζ) (pointY q ζ) hζpt := by
            rw [add_comm, ← succ_nsmul]

end TateCurve

namespace TateCurve

variable {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  [CharZero K] [DecidableEq K] [IsAlgClosed K]
variable {q ζ t : K} {p : ℕ}

section UnconditionalCascade

theorem muTranslation_unconditional (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp5 : 5 ≤ p)
    (hpp : p.Prime) (hζ : IsPrimitiveRoot ζ p) : MuTranslation q ζ p :=
  muTranslation_of_symAddHyps_of_diffHyp (symAddHyps_unconditional hq0 hq)
    (diffHyp_unconditional hq0 (by exact_mod_cast hq)) hq0 hq hp5 hpp hζ

theorem nsmul_prime_eq_zero_unconditional (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u) {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 (symAddHyps_unconditional hq0 hq) hq0 hq hu0 hu hpow hp hodd hns

theorem eq_zpow_mul_of_pointXY_eq_unconditional (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    {u v : K} (hu0 : u ≠ 0) (hv0 : v ≠ 0) (hu : OffLattice q u) (hv : OffLattice q v)
    {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 :=
  eq_zpow_mul_of_pointXY_eq (symAddHyps_unconditional hq0 hq) hq0 hq hu0 hv0 hu hv
    hpu hpv hp hodd hX hY

end UnconditionalCascade

section Parametrization

private lemma zeta_ne_zero (hp : p.Prime) (hζ : IsPrimitiveRoot ζ p) : ζ ≠ 0 := by
  intro h0
  have hζp : ζ ^ p = 1 := hζ.pow_eq_one
  rw [h0, zero_pow hp.ne_zero] at hζp
  exact zero_ne_one hζp

private lemma troot_ne_zero (hq0 : q ≠ 0) (hp : p.Prime) (ht : t ^ p = q) : t ≠ 0 := by
  intro h0
  exact hq0 (by rw [← ht, h0, zero_pow hp.ne_zero])

variable (q ζ t) in

noncomputable def tateTorsionPoint (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (i j : ℕ) : (curve q).toAffine.Point :=
  if hij : i < p ∧ j < p ∧ ¬(i = 0 ∧ j = 0) then
    Point.some (pointX q (ζ ^ i * t ^ j)) (pointY q (ζ ^ i * t ^ j))
      (nonsingular_point hq0 hq
        (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht))
        (tateParam_offLattice hq0 hq hζ ht hij.1 hij.2.1 hij.2.2))
  else 0

lemma tateTorsionPoint_spec (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j : ℕ} (hi : i < p) (hj : j < p) (hij : ¬(i = 0 ∧ j = 0)) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht i j
      = Point.some (pointX q (ζ ^ i * t ^ j)) (pointY q (ζ ^ i * t ^ j))
          (nonsingular_point hq0 hq
            (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht))
            (tateParam_offLattice hq0 hq hζ ht hi hj hij)) := by
  rw [tateTorsionPoint, dif_pos ⟨hi, hj, hij⟩]

@[simp] lemma tateTorsionPoint_zero_zero (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht 0 0 = 0 := by
  rw [tateTorsionPoint, dif_neg (fun h => h.2.2 ⟨rfl, rfl⟩)]

lemma tateTorsionPoint_ne_zero (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j : ℕ} (hi : i < p) (hj : j < p) (hij : ¬(i = 0 ∧ j = 0)) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht i j ≠ 0 := by
  rw [tateTorsionPoint_spec hq0 hq hp hζ ht hi hj hij]
  exact Point.some_ne_zero _

lemma nsmul_tateTorsionPoint (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (i j : ℕ) :
    p • tateTorsionPoint q ζ t hq0 hq hp hζ ht i j = 0 := by
  by_cases hij : i < p ∧ j < p ∧ ¬(i = 0 ∧ j = 0)
  · rw [tateTorsionPoint_spec hq0 hq hp hζ ht hij.1 hij.2.1 hij.2.2]
    exact nsmul_prime_eq_zero_unconditional hq0 hq
      (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht))
      (tateParam_offLattice hq0 hq hζ ht hij.1 hij.2.1 hij.2.2)
      (tateParam_pow hζ.pow_eq_one ht i j) hp (hp.odd_of_ne_two (by omega)) _
  · rw [tateTorsionPoint, dif_neg hij, smul_zero]

lemma tateTorsionPoint_mem (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) (i j : ℕ) :
    tateTorsionPoint q ζ t hq0 hq hp hζ ht i j
      ∈ Submodule.torsionBy ℤ (curve q).toAffine.Point p := by
  rw [Submodule.mem_torsionBy_iff, natCast_zsmul]
  exact nsmul_tateTorsionPoint hq0 hq hp hp5 hζ ht i j

lemma tateTorsionPoint_injOn (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    {i j i' j' : ℕ} (hi : i < p) (hj : j < p) (hi' : i' < p)
    (hj' : j' < p)
    (hpp : tateTorsionPoint q ζ t hq0 hq hp hζ ht i j
      = tateTorsionPoint q ζ t hq0 hq hp hζ ht i' j') : i = i' ∧ j = j' := by
  have hζ0 : ζ ≠ 0 := zeta_ne_zero hp hζ
  have ht0 : t ≠ 0 := troot_ne_zero hq0 hp ht
  by_cases hij : i = 0 ∧ j = 0
  · by_cases hij' : i' = 0 ∧ j' = 0
    · exact ⟨hij.1.trans hij'.1.symm, hij.2.trans hij'.2.symm⟩
    · exfalso
      rw [hij.1, hij.2, tateTorsionPoint_zero_zero] at hpp
      exact tateTorsionPoint_ne_zero hq0 hq hp hζ ht hi' hj' hij' hpp.symm
  · by_cases hij' : i' = 0 ∧ j' = 0
    · exfalso
      rw [hij'.1, hij'.2, tateTorsionPoint_zero_zero] at hpp
      exact tateTorsionPoint_ne_zero hq0 hq hp hζ ht hi hj hij hpp
    · rw [tateTorsionPoint_spec hq0 hq hp hζ ht hi hj hij,
        tateTorsionPoint_spec hq0 hq hp hζ ht hi' hj' hij', Point.some.injEq] at hpp
      obtain ⟨k, hk⟩ := eq_zpow_mul_of_pointXY_eq_unconditional hq0 hq
        (tateParam_ne_zero hζ0 ht0) (tateParam_ne_zero hζ0 ht0)
        (tateParam_offLattice hq0 hq hζ ht hi hj hij)
        (tateParam_offLattice hq0 hq hζ ht hi' hj' hij')
        (tateParam_pow hζ.pow_eq_one ht i j) (tateParam_pow hζ.pow_eq_one ht i' j')
        hp (hp.odd_of_ne_two (by omega)) hpp.1 hpp.2
      exact tateParam_class_eq hq0 hq hζ ht ht0 hi hj hi' hj' hk

variable (q ζ t) in

noncomputable def tateTorsionEquiv (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) :
    (Fin p × Fin p) ≃ ((curve q).n_torsionGen p) := by
  refine Equiv.ofBijective
    (fun ij => ⟨tateTorsionPoint q ζ t hq0 hq hp hζ ht (ij.1 : ℕ) (ij.2 : ℕ),
      tateTorsionPoint_mem hq0 hq hp hp5 hζ ht (ij.1 : ℕ) (ij.2 : ℕ)⟩) ⟨?_, ?_⟩
  · rintro ⟨i, j⟩ ⟨i', j'⟩ hff
    obtain ⟨h1, h2⟩ := tateTorsionPoint_injOn hq0 hq hp hp5 hζ ht i.isLt j.isLt i'.isLt j'.isLt
      (congrArg Subtype.val hff)
    rw [Prod.mk.injEq]
    exact ⟨Fin.ext h1, Fin.ext h2⟩
  · rintro ⟨R, hR⟩
    have hRkill : p • R = 0 := by
      have h := (Submodule.mem_torsionBy_iff _ _).mp hR
      rwa [natCast_zsmul] at h
    rcases eq_zero_or_eq_tateParam_unconditional hq0 hq hp hp5 hζ ht R hRkill with
      h0 | ⟨i, j, hi, hj, hij, hns, hRe⟩
    · refine ⟨(⟨0, hp.pos⟩, ⟨0, hp.pos⟩), ?_⟩
      apply Subtype.ext
      show tateTorsionPoint q ζ t hq0 hq hp hζ ht 0 0 = R
      rw [tateTorsionPoint_zero_zero, h0]
    · refine ⟨(⟨i, hi⟩, ⟨j, hj⟩), ?_⟩
      apply Subtype.ext
      show tateTorsionPoint q ζ t hq0 hq hp hζ ht i j = R
      rw [tateTorsionPoint_spec hq0 hq hp hζ ht hi hj hij, hRe]

theorem natCard_n_torsionGen_curve (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q) :
    Nat.card ((curve q).n_torsionGen p) = p ^ 2 := by
  rw [← Nat.card_congr (tateTorsionEquiv q ζ t hq0 hq hp hp5 hζ ht),
    Nat.card_eq_fintype_card, Fintype.card_prod, Fintype.card_fin, sq]

end Parametrization

section GroupStructure

theorem tateTorsionPoint_zeta_mul (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime) (hp5 : 5 ≤ p)
    (hζ : IsPrimitiveRoot ζ p) {a : ℕ} (ha1 : 1 ≤ a) (hap : a < p)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u) (hau : OffLattice q (ζ ^ a * u))
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ a)) (pointY q (ζ ^ a)))
    (h₃ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q (ζ ^ a * u)) (pointY q (ζ ^ a * u)) h₁ :
        (curve q).toAffine.Point)
      = Point.some (pointX q (ζ ^ a)) (pointY q (ζ ^ a)) h₂
          + Point.some (pointX q u) (pointY q u) h₃ :=
  muTranslation_unconditional hq0 hq hp5 hp hζ a ha1 hap u hu0 hu hau h₁ h₂ h₃

theorem tateTorsionPoint_fst_eq_nsmul (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (hζns : (curve q).toAffine.Nonsingular (pointX q ζ) (pointY q ζ))
    {i : ℕ} (hi1 : 1 ≤ i) (hip : i < p)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q (ζ ^ i)) (pointY q (ζ ^ i))) :
    (Point.some (pointX q (ζ ^ i)) (pointY q (ζ ^ i)) h₁ : (curve q).toAffine.Point)
      = i • Point.some (pointX q ζ) (pointY q ζ) hζns :=
  zeta_pow_point_eq_nsmul (muTranslation_unconditional hq0 hq hp5 hp hζ) hq0 hq hp hζ ht
    hζns i hi1 hip h₁

theorem tateTorsionPoint_inv (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1)
    {u : K} (hu0 : u ≠ 0) (hu : OffLattice q u)
    (h₁ : (curve q).toAffine.Nonsingular (pointX q u⁻¹) (pointY q u⁻¹))
    (h₂ : (curve q).toAffine.Nonsingular (pointX q u) (pointY q u)) :
    (Point.some (pointX q u⁻¹) (pointY q u⁻¹) h₁ : (curve q).toAffine.Point)
      = -Point.some (pointX q u) (pointY q u) h₂ :=
  point_inv_eq_neg hq0 hq hu0 hu h₁ h₂

end GroupStructure

section GaloisAction

private lemma map_tateParam (σ : K →+* K) {e c : ℕ} (hσζ : σ ζ = ζ ^ e)
    (hσt : σ t = ζ ^ c * t) (i j : ℕ) :
    σ (ζ ^ i * t ^ j) = ζ ^ (e * i + c * j) * t ^ j := by
  rw [map_mul, map_pow, map_pow, hσζ, hσt, mul_pow, ← pow_mul, ← pow_mul, pow_add]
  ring

theorem map_pointX_tateParam (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (σ : K →+* K) (hσ : Isometry ⇑σ) (hσq : σ q = q) {e c : ℕ}
    (hσζ : σ ζ = ζ ^ e) (hσt : σ t = ζ ^ c * t) (i j : ℕ) :
    σ (pointX q (ζ ^ i * t ^ j)) = pointX q (ζ ^ (e * i + c * j) * t ^ j) := by
  rw [map_pointX σ hσ hσq hq0 hq
    (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht)),
    map_tateParam σ hσζ hσt]

theorem map_pointY_tateParam (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (σ : K →+* K) (hσ : Isometry ⇑σ) (hσq : σ q = q) {e c : ℕ}
    (hσζ : σ ζ = ζ ^ e) (hσt : σ t = ζ ^ c * t) (i j : ℕ) :
    σ (pointY q (ζ ^ i * t ^ j)) = pointY q (ζ ^ (e * i + c * j) * t ^ j) := by
  rw [map_pointY σ hσ hσq hq0 hq
    (tateParam_ne_zero (zeta_ne_zero hp hζ) (troot_ne_zero hq0 hp ht)),
    map_tateParam σ hσζ hσt]

theorem map_pointX_tateParam_toric (hq0 : q ≠ 0) (hq : ‖q‖₊ < 1) (hp : p.Prime)
    (hζ : IsPrimitiveRoot ζ p) (ht : t ^ p = q)
    (σ : K →+* K) (hσ : Isometry ⇑σ) (hσq : σ q = q) {e c : ℕ}
    (hσζ : σ ζ = ζ ^ e) (hσt : σ t = ζ ^ c * t) (i : ℕ) :
    σ (pointX q (ζ ^ i * t ^ 0)) = pointX q (ζ ^ (e * i) * t ^ 0) := by
  have h := map_pointX_tateParam hq0 hq hp hζ ht σ hσ hσq hσζ hσt i 0
  simpa using h

end GaloisAction

end TateCurve

Definitions/Def_TateCurve_TorsionParametrization.lean

Parametrising the p-torsion of the Tate curve