The Farey dissection of positive order is nonempty

Proved

Farey.one_one_mem_pairs

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

analytic-number-theorycircle-methodfareynumber-theory

For every $P \ge 1$ the pair $(1,1)$ — representing the fraction $1/1$ — lies in the Farey dissection of order $P$ .

P \ge 1 \;\Longrightarrow\; (1,1) \in \mathcal{F}_P.

In particular the dissection is nonempty, which is what lets one split a sum over the arcs by isolating a distinguished term. In the circle method the arc at $1/1$ is the one carrying the main term of the asymptotic.

Preamble

import Definitions.Def_Farey
import Mathlib

Formal statement

namespace Farey

theorem one_one_mem_pairs {P : ℕ} (hP : 0 < P) : ((1 : ℕ), (1 : ℕ)) ∈ pairs P := 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