Distinct Farey pairs represent distinct fractions

Proved

Farey.pairs_inj

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

analytic-number-theorycircle-methodfareynumber-theory

If two Farey pairs of order $P$ represent the same real number, they are the same pair:

\frac{a}{q} = \frac{a'}{q'} \;\Longrightarrow\; (q,a) = (q',a').

Equivalently, the map $(q,a) \mapsto a/q$ is injective on the dissection. This is exactly what makes the major arcs well defined: each arc is centred at a distinct rational, so distinct pairs give distinct centres and the arcs can be indexed by the pairs themselves. It rests on coprimality — without $\gcd(a,q)=1$ the fraction $2/4$ would duplicate $1/2$ .

Preamble

import Definitions.Def_Farey
import Mathlib

Formal statement

namespace Farey

theorem pairs_inj {P : ℕ} {p p' : ℕ × ℕ} (hp : p ∈ pairs P) (hp' : p' ∈ pairs P)
    (h : (p.2 : ℝ) / (p.1 : ℝ) = (p'.2 : ℝ) / (p'.1 : ℝ)) : p = 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