Hasse bound

DefinitionPrimitive triple of polynomials#✓fully proved

Let \(K\) be a field. Polynomials \(a, b, c \in K[X]\) form a primitive triple when they generate the unit ideal of \(K[X]\), that is, when there are \(u, v, w \in K[X]\) with \(ua + vb + wc = 1\).

def PrimitiveTriple (a b c : K[X]) : Prop :=
  ∃ u v w : K[X], u * a + v * b + w * c = 1

Used by 4

Used byManin degree data for the odd-characteristic normal form · Manin degree data for the characteristic-two normal forms · Polynomials with no common irreducible factor form a primitive triple · Numerator degrees from a primitive presentation of product and sum

TheoremPolynomials with no common irreducible factor form a primitive triple#✓fully proved

Let \(K\) be a field and let \(a, b, c \in K[X]\) with \(c \neq 0\). If no irreducible polynomial in \(K[X]\) divides all of \(a\), \(b\) and \(c\), then \(a, b, c\) form a primitive triple: there are \(u, v, w \in K[X]\) with \(ua + vb + wc = 1\).

theorem primitiveTriple_of_no_common_irreducible {a b c : K[X]}
    (hc : c ≠ 0)
    (h : ∀ p : K[X], Irreducible p → p ∣ a → p ∣ b → p ∣ c → False) :
    PrimitiveTriple a b c

Uses 1 · Used by 3

Statement usesPrimitive triple of polynomials

Used byManin degree data for the odd-characteristic normal form · Manin degree data for the characteristic-two normal forms · Numerator degrees from a primitive presentation of product and sum

TheoremNumerator degrees from a primitive presentation of product and sum#✓fully proved

Let \(K\) be a field, let \(u, v, h \in K[X]\) form a primitive triple with \(h \neq 0\), and let \(x, y \in K(X)\) be nonzero rational functions with \(u/h = xy\) and \(v/h = x + y\) in \(K(X)\). Then \(\deg u = \deg \operatorname{num}(x) + \deg \operatorname{num}(y)\), where \(\operatorname{num}\) denotes the numerator of a rational function written in lowest terms.

theorem projective_first_natDegree {u v h : K[X]}
    (hprimitive : PrimitiveTriple u v h)
    (hh : h ≠ 0) {x y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0)
    (hprod : algebraMap K[X] (RatFunc K) u /
      algebraMap K[X] (RatFunc K) h = x * y)
    (hsum : algebraMap K[X] (RatFunc K) v /
      algebraMap K[X] (RatFunc K) h = x + y) :
    u.natDegree = x.num.natDegree + y.num.natDegree

Uses 2 · Used by 2

Statement usesPrimitive triple of polynomials

Proof usesPolynomials with no common irreducible factor form a primitive triple

Used byManin degree data for the odd-characteristic normal form · Manin degree data for the characteristic-two normal forms

TheoremInteger sequences with constant second difference two#✓fully proved

Let \(d : \mathbb{Z} \to \mathbb{Z}\) satisfy \(d(n-1) + d(n+1) = 2d(n) + 2\) for every integer \(n\), and let \(q, N\) be integers with \(d(0) = q\) and \(d(-1) = N\). Then \(d(n) = n^2 + (q + 1 - N)n + q\) for every integer \(n\).

theorem eq_quadratic_of_recurrence (d : ℤ → ℤ) (q N : ℤ)
    (hrec : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2)
    (hzero : d 0 = q) (hnegOne : d (-1) = N) (n : ℤ) :
    d n = n ^ 2 + (q + 1 - N) * n + q

Used by 1

Used byHasse bound from Manin degree data

TheoremDiscriminant bound for a nonnegative integral quadratic without adjacent zeros#✓fully proved

Let \(a, q \in \mathbb{Z}\). If \(n^2 + an + q \ge 0\) for every integer \(n\) and there is no integer \(n\) with \(n^2 + an + q = 0\) and \((n+1)^2 + a(n+1) + q = 0\), then \(a^2 \le 4q\).

theorem sq_le_four_mul_of_quadratic_nonnegative {a q : ℤ}
    (hnonneg : ∀ n : ℤ, 0 ≤ n ^ 2 + a * n + q)
    (hnotTwoZeros : ∀ n : ℤ,
      n ^ 2 + a * n + q = 0 → (n + 1) ^ 2 + a * (n + 1) + q = 0 → False) :
    a ^ 2 ≤ 4 * q

Used by 1

Used byHasse bound from Manin degree data

StructureManin degree data#✓fully proved

For natural numbers \(q\) and \(N\), Manin degree data for \(q\) and \(N\) is a sequence \(d : \mathbb{Z} \to \mathbb{N}\) such that \(d(0) = q\), \(d(-1) = N\), \(d(n-1) + d(n+1) = 2d(n) + 2\) for every integer \(n\), and there is no integer \(n\) with \(d(n) = d(n+1) = 0\).

These are the properties of the polynomial-degree sequence used in Manin's proof of the Hasse bound.

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

Used by 9

Used byHasse bound from Manin degree data · Hasse bound for the odd-characteristic normal form · Hasse bound for the characteristic-two normal forms · Manin degree data over the field with four elements · Manin degree data over the field with three elements · Manin degree data over the field with two elements · Manin degree data for the odd-characteristic normal form · Manin degree data for the characteristic-two normal forms · Manin degree data from a quadratic

DefinitionManin degree data from a quadratic#✓fully proved

Let \(q\) and \(N\) be natural numbers and put \(a = q + 1 - N \in \mathbb{Z}\). Suppose \(n^2 + an + q \ge 0\) for every integer \(n\), and there is no integer \(n\) at which both \(n^2 + an + q\) and \((n+1)^2 + a(n+1) + q\) vanish. Then the sequence \(d(n) = n^2 + an + q\) is Manin degree data for \(q\) and \(N\).

MathlibExt.AlgebraicGeometry.EllipticCurve.ManinDegreeData.ofQuadratic · 27 lines

def ofQuadratic (q N : ℕ) (a : ℤ) (ha : a = (q : ℤ) + 1 - (N : ℤ))
    (hnonneg : ∀ n, 0 ≤ n ^ 2 + a * n + q)
    (hnoAdjacent : ∀ n, n ^ 2 + a * n + q = 0 →
      (n + 1) ^ 2 + a * (n + 1) + q = 0 → False) : ManinDegreeData q N where
  d n := (n ^ 2 + a * n + q).toNat
  zero := by simp
  negOne := by
    have h := hnonneg (-1)
    apply Int.ofNat_injective
    change (((-1 : ℤ) ^ 2 + a * (-1) + q).toNat : ℤ) = (N : ℤ)
    rw [Int.toNat_of_nonneg h]
    simp [ha]
    ring
  recurrence n := by
    have hm := hnonneg (n - 1)
    have hn := hnonneg n
    have hp := hnonneg (n + 1)
    apply Int.ofNat_injective
    change ((((n - 1) ^ 2 + a * (n - 1) + q).toNat : ℕ) : ℤ) +
        (((n + 1) ^ 2 + a * (n + 1) + q).toNat : ℕ) =
      2 * (((n ^ 2 + a * n + q).toNat : ℕ) : ℤ) + 2
    rw [Int.toNat_of_nonneg hm, Int.toNat_of_nonneg hn, Int.toNat_of_nonneg hp]
    ring
  noAdjacentZeros n hn hn1 := by
    apply hnoAdjacent n
    · exact le_antisymm (Int.toNat_eq_zero.mp hn) (hnonneg n)
    · exact le_antisymm (Int.toNat_eq_zero.mp hn1) (hnonneg (n + 1))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

  d : ℤ → ℕ

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:91

Uses 1 · Used by 3

Statement usesManin degree data

Used byManin degree data over the field with four elements · Manin degree data over the field with three elements · Manin degree data over the field with two elements

TheoremHasse bound from Manin degree data#✓fully proved

Let \(q\) and \(N\) be natural numbers. If there is Manin degree data for \(q\) and \(N\), then \((q + 1 - N)^2 \le 4q\), computed in the integers.

theorem hasse_bound {q N : ℕ} (data : ManinDegreeData q N) :
    (((q : ℤ) + 1 - (N : ℤ)) ^ 2 ≤ 4 * (q : ℤ))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

Uses 3 · Used by 2

Statement usesManin degree data

Proof usesInteger sequences with constant second difference two · Discriminant bound for a nonnegative integral quadratic without adjacent zeros

Used byHasse bound for the odd-characteristic normal form · Hasse bound for the characteristic-two normal forms

TheoremManin degree data over the field with three elements#✓fully proved

Let \(F\) be a field with exactly three elements, let \(W\) be any Weierstrass curve over \(F\), and let \(N\) be the number of nonsingular points of \(W\) over \(F\), including the point at infinity. Then there is Manin degree data for \((3, N)\): a function \(d : \mathbb{Z} \to \mathbb{N}\) with \(d(0) = 3\), \(d(-1) = N\), \(d(n - 1) + d(n + 1) = 2 d(n) + 2\) for every integer \(n\), and no integer \(n\) with \(d(n) = d(n + 1) = 0\).

The proof needs only the elementary bound \(N \le 2 \cdot 3 + 1\).

public theorem manin_degree_data_of_card_eq_three [Finite F] (hF : Nat.card F = 3)
    (W : WeierstrassCurve F) :
    Nonempty (MathlibExt.AlgebraicGeometry.EllipticCurve.ManinDegreeData
      (Nat.card F) (Nat.card W.toAffine.Point))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

Uses 3 · Used by 1

Statement usesManin degree data

Proof usesManin degree data from a quadratic · Upper bound on the point count

Used byManin degree data for the odd-characteristic normal form

TheoremManin degree data for the odd-characteristic normal form#✓fully proved

Let \(F\) be a finite field with \(q\) elements, let \(W\) be a Weierstrass curve \(y^2 = x^3 + a_2 x^2 + a_4 x + a_6\) over \(F\) (that is, \(a_1 = a_3 = 0\)) with nonzero discriminant, and let \(N\) be the number of points of \(W\) over \(F\), including the point at infinity. Then there is Manin degree data for \((q, N)\): a function \(d : \mathbb{Z} \to \mathbb{N}\) with \(d(0) = q\), \(d(-1) = N\), \(d(n - 1) + d(n + 1) = 2 d(n) + 2\) for every integer \(n\), and no integer \(n\) with \(d(n) = d(n + 1) = 0\).

public theorem manin_degree_data_of_isCharNeTwoNF [Finite F]
    (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharNeTwoNF] :
    Nonempty (MathlibExt.AlgebraicGeometry.EllipticCurve.ManinDegreeData
      (Nat.card F) (Nat.card W.toAffine.Point))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

Uses 6 · Used by 1

Statement usesManin degree data

Proof usesPrimitive triple of polynomials · Polynomials with no common irreducible factor form a primitive triple · Numerator degrees from a primitive presentation of product and sum · Manin degree data over the field with three elements · Point count from affine solutions

Used byHasse bound for the odd-characteristic normal form

TheoremHasse bound for the odd-characteristic normal form#✓fully proved

Let \(F\) be a finite field with \(q\) elements and let \(W\) be a Weierstrass curve \(y^2 = x^3 + a_2 x^2 + a_4 x + a_6\) over \(F\) (that is, \(a_1 = a_3 = 0\)) with nonzero discriminant. If \(N\) is the number of points of \(W\) over \(F\), including the point at infinity, then \((q + 1 - N)^2 \le 4q\).

public theorem hasse_bound_of_isCharNeTwoNF [Finite F]
    (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharNeTwoNF] :
    (((Nat.card F : ℤ) + 1 - (Nat.card W.toAffine.Point : ℤ)) ^ 2 ≤
      4 * (Nat.card F : ℤ))

Uses 3 · Used by 1

Proof usesManin degree data · Hasse bound from Manin degree data · Manin degree data for the odd-characteristic normal form

Used byHasse bound

TheoremManin degree data over the field with two elements#✓fully proved

Let \(F\) be a field with exactly two elements, let \(W\) be any Weierstrass curve over \(F\), and let \(N\) be the number of nonsingular points of \(W\) over \(F\), including the point at infinity. Then there is Manin degree data for \((2, N)\): a function \(d : \mathbb{Z} \to \mathbb{N}\) with \(d(0) = 2\), \(d(-1) = N\), \(d(n - 1) + d(n + 1) = 2 d(n) + 2\) for every integer \(n\), and no integer \(n\) with \(d(n) = d(n + 1) = 0\).

The proof needs only the elementary bound \(N \le 2 \cdot 2 + 1\).

theorem manin_degree_data_of_card_eq_two [Finite F] (hF : Nat.card F = 2)
    (W : WeierstrassCurve F) :
    Nonempty (MathlibExt.AlgebraicGeometry.EllipticCurve.ManinDegreeData
      (Nat.card F) (Nat.card W.toAffine.Point))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

Uses 3 · Used by 1

Statement usesManin degree data

Proof usesManin degree data from a quadratic · Upper bound on the point count

Used byManin degree data for the characteristic-two normal forms

TheoremManin degree data over the field with four elements#✓fully proved

Let \(F\) be a field with exactly four elements, let \(W\) be any Weierstrass curve over \(F\), and let \(N\) be the number of nonsingular points of \(W\) over \(F\), including the point at infinity. Then there is Manin degree data for \((4, N)\): a function \(d : \mathbb{Z} \to \mathbb{N}\) with \(d(0) = 4\), \(d(-1) = N\), \(d(n - 1) + d(n + 1) = 2 d(n) + 2\) for every integer \(n\), and no integer \(n\) with \(d(n) = d(n + 1) = 0\).

The proof needs only the elementary bound \(N \le 2 \cdot 4 + 1\).

theorem manin_degree_data_of_card_eq_four [Finite F] (hF : Nat.card F = 4)
    (W : WeierstrassCurve F) :
    Nonempty (MathlibExt.AlgebraicGeometry.EllipticCurve.ManinDegreeData
      (Nat.card F) (Nat.card W.toAffine.Point))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

Uses 3 · Used by 1

Statement usesManin degree data

Proof usesManin degree data from a quadratic · Upper bound on the point count

Used byManin degree data for the characteristic-two normal forms

TheoremManin degree data for the characteristic-two normal forms#✓fully proved

Let \(F\) be a finite field of characteristic \(2\) with \(q\) elements, let \(W\) be a Weierstrass curve over \(F\) with nonzero discriminant that is in one of the two characteristic-two normal forms \(y^2 + xy = x^3 + a_2 x^2 + a_6\) (that is, \(a_1 = 1\) and \(a_3 = a_4 = 0\)) or \(y^2 + a_3 y = x^3 + a_4 x + a_6\) (that is, \(a_1 = a_2 = 0\)), and let \(N\) be the number of points of \(W\) over \(F\), including the point at infinity. Then there is Manin degree data for \((q, N)\): a function \(d : \mathbb{Z} \to \mathbb{N}\) with \(d(0) = q\), \(d(-1) = N\), \(d(n - 1) + d(n + 1) = 2 d(n) + 2\) for every integer \(n\), and no integer \(n\) with \(d(n) = d(n + 1) = 0\).

theorem manin_degree_data_of_isCharTwoNF [Finite F] [CharP F 2]
    (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoNF] :
    Nonempty (MathlibExt.AlgebraicGeometry.EllipticCurve.ManinDegreeData
      (Nat.card F) (Nat.card W.toAffine.Point))

structure ManinDegreeData (q N : ℕ) where
  /-- The numerator degree attached to the point indexed by an integer. -/
  d : ℤ → ℕ
  /-- Frobenius has degree `q`. -/
  zero : d 0 = q
  /-- Frobenius minus the identity has degree equal to the rational point count. -/
  negOne : d (-1) = N
  /-- The degree sequence has constant second difference two. -/
  recurrence : ∀ n, d (n - 1) + d (n + 1) = 2 * d n + 2
  /-- Consecutive points in the sequence cannot both have degree zero. -/
  noAdjacentZeros : ∀ n, d n = 0 → d (n + 1) = 0 → False

MathlibExt/AlgebraicGeometry/EllipticCurve/ManinSequence.lean:89

Uses 7 · Used by 1

Statement usesManin degree data

Proof usesPrimitive triple of polynomials · Polynomials with no common irreducible factor form a primitive triple · Numerator degrees from a primitive presentation of product and sum · Manin degree data over the field with four elements · Manin degree data over the field with two elements · Point count from affine solutions

Used byHasse bound for the characteristic-two normal forms

TheoremHasse bound for the characteristic-two normal forms#✓fully proved

Let \(F\) be a finite field of characteristic \(2\) with \(q\) elements and let \(W\) be a Weierstrass curve over \(F\) with nonzero discriminant that is in one of the two characteristic-two normal forms \(y^2 + xy = x^3 + a_2 x^2 + a_6\) (that is, \(a_1 = 1\) and \(a_3 = a_4 = 0\)) or \(y^2 + a_3 y = x^3 + a_4 x + a_6\) (that is, \(a_1 = a_2 = 0\)). If \(N\) is the number of points of \(W\) over \(F\), including the point at infinity, then \((q + 1 - N)^2 \le 4q\).

theorem hasse_bound_of_isCharTwoNF [Finite F] [CharP F 2]
    (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoNF] :
    (((Nat.card F : ℤ) + 1 - (Nat.card W.toAffine.Point : ℤ)) ^ 2 ≤
      4 * (Nat.card F : ℤ))

Uses 3 · Used by 3

Proof usesManin degree data · Hasse bound from Manin degree data · Manin degree data for the characteristic-two normal forms

Used byHasse bound · Hasse bound for the supersingular characteristic-two normal form · Hasse bound for the ordinary characteristic-two normal form

TheoremHasse bound for the ordinary characteristic-two normal form#✓fully proved

Let \(F\) be a finite field of characteristic \(2\) with \(q\) elements and let \(W\) be a Weierstrass curve \(y^2 + xy = x^3 + a_2 x^2 + a_6\) over \(F\) (that is, \(a_1 = 1\) and \(a_3 = a_4 = 0\)) with nonzero discriminant. If \(N\) is the number of points of \(W\) over \(F\), including the point at infinity, then \((q + 1 - N)^2 \le 4q\).

theorem hasse_bound_of_isCharTwoJNeZeroNF [Finite F] [CharP F 2]
    (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoJNeZeroNF] :
    (((Nat.card F : ℤ) + 1 - (Nat.card W.toAffine.Point : ℤ)) ^ 2 ≤
      4 * (Nat.card F : ℤ))

Uses 1

Proof usesHasse bound for the characteristic-two normal forms

TheoremHasse bound for the supersingular characteristic-two normal form#✓fully proved

Let \(F\) be a finite field of characteristic \(2\) with \(q\) elements and let \(W\) be a Weierstrass curve \(y^2 + a_3 y = x^3 + a_4 x + a_6\) over \(F\) (that is, \(a_1 = a_2 = 0\)) with nonzero discriminant. If \(N\) is the number of points of \(W\) over \(F\), including the point at infinity, then \((q + 1 - N)^2 \le 4q\).

theorem hasse_bound_of_isCharTwoJEqZeroNF [Finite F] [CharP F 2]
    (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoJEqZeroNF] :
    (((Nat.card F : ℤ) + 1 - (Nat.card W.toAffine.Point : ℤ)) ^ 2 ≤
      4 * (Nat.card F : ℤ))

Uses 1

Proof usesHasse bound for the characteristic-two normal forms

TheoremHasse bound#✓fully proved

Let \(F\) be a finite field with \(q\) elements and let \(E\) be an elliptic curve over \(F\) given by a Weierstrass equation. If \(N\) is the number of points of \(E\) with coordinates in \(F\), including the point at infinity, then \((q + 1 - N)^2 \le 4q\) in \(\mathbb{Z}\).

Proof: Manin's elementary polynomial-degree argument on a twist over the rational function field \(F(t)\), done separately for the odd-characteristic and characteristic-two normal forms. In characteristic two the point count uses the fibres of the additive maps \(y \mapsto y^2 + by\) with \(b \in F\), followed by the same projective neighboring-degree recurrence, as in Chahal--Soomro--Top, Rocky Mountain J. Math. 44 (2014).

public theorem hasse_bound {F : Type*} [Field F] [Fintype F] [DecidableEq F]
    (W : WeierstrassCurve F) [W.IsElliptic] :
    (((Nat.card F : ℤ) + 1 - (Nat.card (W.toAffine.Point) : ℤ)) ^ 2 ≤
      4 * (Nat.card F : ℤ))

Sources

H. Hasse, J. Reine Angew. Math. 1936; modern Silverman, The Arithmetic of Elliptic Curves, 2nd ed.; Lean states integral squared form of |N-(q+1)| ≤ 2√q including point at infinity.

Uses 3

Proof usesHasse bound for the odd-characteristic normal form · Hasse bound for the characteristic-two normal forms · Variable changes preserve the point count

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.