$c_1(n)=1$

Proved

Vino.ramanujan_one

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

analytic-number-theorycircle-methodnumber-theoryramanujan-sums

For the trivial modulus,

c_1(n)=1\qquad\text{for every }n\in\mathbb Z.

Only the residue $a=0$ occurs and it contributes $e(0)=1$ . This is the multiplicative unit of the singular series: the $q=1$ term of $\sum_q \mu(q)c_q(n)/\varphi(q)^3$ equals $1$ .

Preamble

import Definitions.Def_Vino_ramanujan
import Mathlib.Data.Nat.Totient
open Finset

Formal statement

namespace Vino

theorem ramanujan_one (n : ℤ) : ramanujan 1 n = 1 := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Section 2.6 and Chapter 3; G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford University Press, 2008, Section 16.6 (Ramanujan's sum c_q(n)).

View graph

c1(n)=1c_1(n)=1c1​(n)=1

$c_1(n)=1$