7. The Hasse bound🔗

Theorem7.1

Statement uses 2

Statement dependency previews

Preview

Theorem 3.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

(Hasse bound from positivity + point count.) Given the positivity of the degree form (Theorem 3.3) and the point-count identity (Theorem 4.4), \bigl|\,\#E(\mathbb{F}_q) - (q+1)\,\bigr| \;\le\; 2\sqrt{q}. This is the witness-parametric assembly that isolates the pure-arithmetic core from the geometric input.

Lean code for Theorem7.1●2 theorems

theoremdefined in HasseWeil/Hasse/QuadraticForm.lean

complete

theorem HasseWeil.hasse_bound_of_qf_nonneg_witnesses.{u_1} {K : Type u_1}
  [Field K] [Fintype K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] [Fintype W.toAffine.Point]
  (t : ℤ)
  (h_pc :
    ↑(HasseWeil.pointCount W.toAffine) = ↑(Fintype.card K) + 1 - t)
  (h_qf_nonneg :
    ∀ (r s : ℤ), 0 ≤ ↑(Fintype.card K) * r ^ 2 - t * r * s + s ^ 2) :
  |↑(HasseWeil.pointCount W.toAffine) - ↑(Fintype.card K) - 1| ≤
    2 * √↑(Fintype.card K)

theorem HasseWeil.hasse_bound_of_qf_nonneg_witnesses.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point] (t : ℤ)
  (h_pc :
    ↑(HasseWeil.pointCount W.toAffine) =
      ↑(Fintype.card K) + 1 - t)
  (h_qf_nonneg :
    ∀ (r s : ℤ),
      0 ≤
        ↑(Fintype.card K) * r ^ 2 -
            t * r * s +
          s ^ 2) :
  |↑(HasseWeil.pointCount W.toAffine) -
          ↑(Fintype.card K) -
        1| ≤
    2 * √↑(Fintype.card K)

**Hasse bound, non-negativity form**. Same as `hasse_bound_of_t_witness`
but consumes a non-negativity hypothesis on the QF rather than an isogeny
family + degree-equality witness.

theoremdefined in HasseWeil/Hasse/QuadraticForm.lean

complete

theorem HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses.{u_1} {K : Type u_1}
  [Field K] [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] [Fintype W.toAffine.Point]
  (β_pc : HasseWeil.Isogeny W.toAffine W.toAffine)
  (h_pc_hom :
    β_pc.toAddMonoidHom =
      AddMonoidHom.id W.toAffine.Point -
        (HasseWeil.frobeniusIsog W).toAddMonoidHom)
  (h_pc_ker_deg : Nat.card ↥β_pc.kernel = β_pc.degree)
  (h_qf_nonneg :
    ∀ (r s : ℤ),
      0 ≤
        ↑(Fintype.card K) * r ^ 2 -
            HasseWeil.isogTrace (HasseWeil.frobeniusIsog W) β_pc * r *
              s +
          s ^ 2) :
  |↑(HasseWeil.pointCount W.toAffine) - ↑(Fintype.card K) - 1| ≤
    2 * √↑(Fintype.card K)

theorem HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point]
  (β_pc :
    HasseWeil.Isogeny W.toAffine
      W.toAffine)
  (h_pc_hom :
    β_pc.toAddMonoidHom =
      AddMonoidHom.id W.toAffine.Point -
        (HasseWeil.frobeniusIsog
            W).toAddMonoidHom)
  (h_pc_ker_deg :
    Nat.card ↥β_pc.kernel = β_pc.degree)
  (h_qf_nonneg :
    ∀ (r s : ℤ),
      0 ≤
        ↑(Fintype.card K) * r ^ 2 -
            HasseWeil.isogTrace
                  (HasseWeil.frobeniusIsog
                    W)
                  β_pc *
                r *
              s +
          s ^ 2) :
  |↑(HasseWeil.pointCount W.toAffine) -
          ↑(Fintype.card K) -
        1| ≤
    2 * √↑(Fintype.card K)

**Fully-chained Hasse bound, non-negativity form**. Replaces the QF
isogeny family + degree-equality witness in `hasse_bound_of_full_witnesses`
by a non-negativity hypothesis on the QF expression with `t` instantiated to
`isogTrace (frobeniusIsog W) β_pc`.

Proof for Theorem 7.1

Proof uses 3

Proof dependency previews

Preview

Theorem 4.4

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Positivity gives t^2 \le 4q (Theorem 5.1), hence |t| \le 2\sqrt q (Theorem 5.2); since \#E(\mathbb{F}_q)-(q+1) = -t (Theorem 4.4), the bound follows.

Theorem7.2

uses 0used by 1✓L∃∀N

(Hasse's theorem.) For an elliptic curve E over a finite field \mathbb{F}_q, \bigl|\,\#E(\mathbb{F}_q) - (q + 1)\,\bigr| \;\le\; 2\sqrt{q}. This is the unconditional, sorry-free hasse_bound, specialised from hasse_bound_unconditional (which assumes only 2 \le \#K).

Lean code for Theorem7.2●2 theorems

theoremdefined in HasseWeil/WeilPairing/HasseBound.lean

complete

theorem HasseWeil.WeilPairing.hasse_bound.{u_1} {K : Type u_1} [Field K]
  [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] [Fintype W.toAffine.Point] :
  |↑(HasseWeil.pointCount W.toAffine) - ↑(Fintype.card K) - 1| ≤
    2 * √↑(Fintype.card K)

theorem HasseWeil.WeilPairing.hasse_bound.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point] :
  |↑(HasseWeil.pointCount W.toAffine) -
          ↑(Fintype.card K) -
        1| ≤
    2 * √↑(Fintype.card K)

**The Hasse bound, hypothesis-free capstone** (Silverman V.1.1):
`|#E(𝔽_q) − q − 1| ≤ 2√q` with no explicit cardinality hypothesis — `2 ≤ #K` is
automatic for a finite field (`Fintype.one_lt_card`).  This is the hypothesis-free
form that replaced the retired `hasse_bound_universal` stub
(`Hasse/OpenLemmaPrimitives.lean`, deleted 2026-06-11).

theoremdefined in HasseWeil/WeilPairing/HasseBound.lean

complete

theorem HasseWeil.WeilPairing.hasse_bound_unconditional.{u_1} {K : Type u_1}
  [Field K] [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K) :
  |↑(HasseWeil.pointCount W.toAffine) - ↑(Fintype.card K) - 1| ≤
    2 * √↑(Fintype.card K)

theorem HasseWeil.WeilPairing.hasse_bound_unconditional.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K) :
  |↑(HasseWeil.pointCount W.toAffine) -
          ↑(Fintype.card K) -
        1| ≤
    2 * √↑(Fintype.card K)

**The unconditional Hasse bound** (Silverman V.1.1): for an elliptic curve `E` over a finite field
`𝔽_q`, `|#E(𝔽_q) − q − 1| ≤ 2√q`, with **no hypotheses** beyond `2 ≤ #K`.

Assembled from `hasse_bound_unconditional_of_baseChange_scalings_coprime` (`FrobMatrixData.lean`) with
the kernel-cardinality degree function `pencilKerCard` and the three base-change scalings
`frobeniusScaling_holds`, `oneSubFrobeniusScaling_holds`, `pencilScaling_holds_coprime`.

Instance bookkeeping: `deg` is fixed before `∀ p r`, so it is taken at the canonical `(p₀, n₀)` of
`FiniteField.card' K`; inside the `hscale` discharge `p = p₀` (`CharP.eq`) and `r = n₀`
(`Nat.pow_right_injective`) are forced.

Proof for Theorem 7.2

Proof uses 4

Proof dependency previews

Preview

Definition 1.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Let t = q + 1 - \#E(\mathbb{F}_q) be the trace of Frobenius (Definition 1.5, Definition 1.1). The degree form on \operatorname{End}(E) is positive semi-definite on the Frobenius pencil, so by the degree-form bound t^2 \le 4q (Theorem 3.4). Passing to square roots gives |t| \le 2\sqrt{q} (Theorem 5.2), and since \#E(\mathbb{F}_q) - (q + 1) = -t, this is the displayed bound.

Theorem7.3

uses 0used by 0✓L∃∀N

(Hasse's theorem — unconditional, axiom-clean, via the Weil pairing.) For an elliptic curve E over a finite field \mathbb{F}_q, \bigl|\,\#E(\mathbb{F}_q) - (q + 1)\,\bigr| \;\le\; 2\sqrt{q}, with no hypotheses, discharging the geometric leaf by base-changing to \overline{K} and running the Weil-pairing determinant machinery on the genuine pencil (Silverman V.1.1).

Lean code for Theorem7.3●2 theorems

theoremdefined in HasseWeil/WeilPairing/HasseAssembly.lean

complete

theorem HasseWeil.WeilPairing.hasse_bound_via_weil_pairing.{u_1} {K : Type u_1}
  [Field K] [Fintype K] [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine] [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K) (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hres :
    ∀ (r s : ℤ),
      ¬↑(ringChar K) ∣ s →
        ∀ (ℓ : ℕ),
          Nat.Prime ℓ →
            ℓ ≠ ringChar K →
              ∃ M,
                M.det = ↑↑(Fintype.card K) ∧
                  (1 - M).det =
                      ↑(↑(Fintype.card K) + 1 -
                          HasseWeil.isogTrace
                            (HasseWeil.frobeniusIsog W)
                            (HasseWeil.isogOneSub_negFrobenius W hq)) ∧
                    (↑r • M - ↑s • 1).det = ↑(deg r s)) :
  |↑(HasseWeil.pointCount W.toAffine) - ↑(Fintype.card K) - 1| ≤
    2 * √↑(Fintype.card K)

theorem HasseWeil.WeilPairing.hasse_bound_via_weil_pairing.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K)
  (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hres :
    ∀ (r s : ℤ),
      ¬↑(ringChar K) ∣ s →
        ∀ (ℓ : ℕ),
          Nat.Prime ℓ →
            ℓ ≠ ringChar K →
              ∃ M,
                M.det =
                    ↑↑(Fintype.card K) ∧
                  (1 - M).det =
                      ↑(↑(Fintype.card
                                K) +
                            1 -
                          HasseWeil.isogTrace
                            (HasseWeil.frobeniusIsog
                              W)
                            (HasseWeil.isogOneSub_negFrobenius
                              W hq)) ∧
                    (↑r • M -
                          ↑s • 1).det =
                      ↑(deg r s)) :
  |↑(HasseWeil.pointCount W.toAffine) -
          ↑(Fintype.card K) -
        1| ≤
    2 * √↑(Fintype.card K)

**The Hasse bound via the Weil pairing** (Silverman V.1.1, the Route-2A capstone milestone).

`|#E(F_q) − q − 1| ≤ 2√q`, assembled from the per-`ℓ` Frobenius-matrix determinant data `hres`
(the Weil-pairing `DET-DEG` output, Silverman III.8.6) via the GAP-QF leaf
`qf_nonneg_skeleton_of_weil_det_data` and the shipped Hasse-bound milestone wiring
`hasse_bound_of_full_qf_nonneg_witnesses` (with the second leaf `ker_deg_skeleton` already closed).

The Weil-pairing route discharges the GAP-QF leaf directly from the determinant
data — bypassing the characteristic-`p` dual-additivity wall.

theoremdefined in HasseWeil/WeilPairing/FrobMatrixData.lean

complete

theorem HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime.{u_1}
  {K : Type u_1} [Field K] [Fintype K] [DecidableEq K]
  (W : WeierstrassCurve K) [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point] (hq : 2 ≤ Fintype.card K) (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hscale :
    ∀ (p r : ℕ) (x : Fact (Nat.Prime p)) (x_1 : CharP K p)
      (x_2 : Fact (Fintype.card K = p ^ r)),
      HasseWeil.WeilPairing.FrobBaseChangeScalingsCoprime W p r
        (AlgebraicClosure K) hq deg) :
  |↑(HasseWeil.pointCount W.toAffine) - ↑(Fintype.card K) - 1| ≤
    2 * √↑(Fintype.card K)

theorem HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime.{u_1}
  {K : Type u_1} [Field K] [Fintype K]
  [DecidableEq K] (W : WeierstrassCurve K)
  [WeierstrassCurve.IsElliptic W.toAffine]
  [Fintype W.toAffine.Point]
  (hq : 2 ≤ Fintype.card K)
  (deg : ℤ → ℤ → ℤ)
  (hdeg_nonneg : ∀ (r s : ℤ), 0 ≤ deg r s)
  (hscale :
    ∀ (p r : ℕ) (x : Fact (Nat.Prime p))
      (x_1 : CharP K p)
      (x_2 :
        Fact (Fintype.card K = p ^ r)),
      HasseWeil.WeilPairing.FrobBaseChangeScalingsCoprime
        W p r (AlgebraicClosure K) hq
        deg) :
  |↑(HasseWeil.pointCount W.toAffine) -
          ↑(Fintype.card K) -
        1| ≤
    2 * √↑(Fintype.card K)

**The unconditional Hasse bound from the coprime-BOTH base-change scaling leaf** (reviewer
round-23, Route B).

`|#E(𝔽_q) − q − 1| ≤ 2√q`, assembled from the single leaf `FrobBaseChangeScalingsCoprime` over
`K̄ = AlgebraicClosure K` via `hres_of_baseChange_scalings_coprime` and the coprime-BOTH
`hasse_bound_via_weil_pairing_both`.  This is the **axiom-clean** capstone: the pencil scaling is
requested only on the genuine locus `p ∤ r' ∧ p ∤ s'`, so the inseparable `p ∣ r'` `sorry` is never
demanded.  Identical instance bookkeeping to `hasse_bound_unconditional_of_baseChange_scalings`.

Proof for Theorem 7.3

Proof uses 4

Proof dependency previews

Preview

Theorem 4.4

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

The per-\ell Frobenius determinant data over \overline{K} gives positivity of the degree form (Theorem 6.3); feeding this into the witness-parametric bound (Theorem 7.1) with the point-count identity (Theorem 4.4) yields the unconditional bound, of which the headline hasse_bound (Theorem 7.2) is the hypothesis-free specialisation.