The Farey dissection of order $P$ has at most $P^2$ arcs

Proved

Farey.card_pairs_le

by dbenbenn · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorycircle-methodfareynumber-theory

The Farey dissection of order $P$ contains at most $P^2$ pairs:

\#\{(q,a) : 1 \le a \le q \le P,\ \gcd(a,q)=1\} \;\le\; P^2.

In the circle method this bounds the number of major arcs, which is what keeps their total contribution controllable. The bound is deliberately crude — the true count is $\sum_{q \le P}\varphi(q) \sim 3P^2/\pi^2$ — but $P^2$ is what the standard estimates need and it costs nothing to prove.

Note. The same statement is already on the platform as ThreePrimes.card_fareyPairs_le, reachable only by importing an 11 KB Vinogradov-specific definition bundle. This copy is stated against the standalone Farey definition so that the dissection can be used without that dependency.

Preamble

import Definitions.Def_Farey
import Mathlib

Formal statement

namespace Farey

theorem card_pairs_le (P : ℕ) : (pairs P).card ≤ P ^ 2 := by
  sorry

end Farey

Source

Standard Farey-dissection facts. See R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge University Press 1997, Chapter 2; Hardy & Wright, An Introduction to the Theory of Numbers, Chapter III.

View graph

The Farey dissection of order PPP has at most P2P^2P2 arcs

The Farey dissection of order $P$ has at most $P^2$ arcs