The Gauss sum for the trivial modulus

Proved

Vino.gaussE_modulus_one

by tabbott · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methoddirichlet-charactersnumber-theory

For the modulus $q=1$ there is a single Dirichlet character and

\tau(\chi)=1.

This is the base case of the major-arc analysis: the arc around $0$ corresponds to $q=1$ , where the character expansion degenerates to the identity $S(\alpha,N)\approx\psi(N)$ and no cancellation is available.

Preamble

import Definitions.Def_Vino_dirichlet
import Definitions.Def_Vino_primes
import Mathlib.NumberTheory.DirichletCharacter.Bounds
open Finset

Formal statement

namespace Vino

theorem gaussE_modulus_one (χ : DirichletCharacter ℂ 1) : gaussE 1 χ = 1 := by sorry

end Vino

Source

H. Davenport, Multiplicative Number Theory, 3rd ed., Springer GTM 74, 2000, Chapters 9 and 26; R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3, Section 3.1.

View graph