The Weil bound for $x^d + y^e = 1$ modulo $p$

Proved

Weil.abs_card_diagonal_zmod_sub_le

by tabbott · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

exponential-sumsfinite-fieldsgauss-sumsnumber-theoryweil-bound

Diagonal equations mod $p$ . Let $p$ be a prime and $d, e \ge 1$ . The number of solutions of $x^d + y^e = 1$ in $\mathbb{Z}/p\mathbb{Z}$ satisfies

\bigl|\#\{(x,y) : x^d + y^e \equiv 1 \bmod p\} - p\bigr| \le (d-1)(e-1)\sqrt p.

For $d = e = 3$ this is the Hasse bound for the Fermat cubic, an elliptic curve; for general $d, e$ it is the Riemann hypothesis for the diagonal curve, obtained here from Jacobi sums alone.

Preamble

import Mathlib.NumberTheory.GaussSum
import Mathlib.NumberTheory.JacobiSum.Basic
import Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
import Mathlib.NumberTheory.MulChar.Lemmas
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.GroupTheory.Index
import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Analysis.Complex.Basic
import Mathlib.Algebra.Field.GeomSum
import Mathlib.Algebra.Order.BigOperators.Group.Finset

set_option autoImplicit false
set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

universe u_1 u_2

open AddChar MulChar Finset

Formal statement

namespace Weil
theorem abs_card_diagonal_zmod_sub_le : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {d e : ℕ}, d ≠ 0 → e ≠ 0 → |(↑(Finset.card {z : ZMod p × ZMod p | Prod.fst z ^ d + Prod.snd z ^ e = 1}) : ℝ) - (↑p : ℝ)| ≤ ((↑d : ℝ) - 1) * ((↑e : ℝ) - 1) * √(↑p : ℝ) := by sorry
end Weil

Source

A. Weil, Numbers of solutions of equations in finite fields, Bull. Amer. Math. Soc. 55 (1949), 497-508 (diagonal equations are the worked example of the Weil conjectures)

View graph

The Weil bound for xd+ye=1x^d + y^e = 1xd+ye=1 modulo ppp

The Weil bound for $x^d + y^e = 1$ modulo $p$