Cauchy-Davenport-Chowla for three sets modulo a prime

Proved

ShaoThreeUnits.cauchy_davenport_chowla

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricsnumber-theory

Let $p$ be prime and let $I$ , $J$ , $K$ be nonempty sets of residues modulo $p$ with $|I| + |J| + |K| \ge p + 2$ . Then every residue $x$ modulo $p$ can be written $x = u + v + w$ with $u \in I$ , $v \in J$ and $w \in K$ .

Mathlib carries the two-set Cauchy-Davenport inequality ZMod.cauchy_davenport. This is the three-set consequence that the induction on prime factors in Section 3 consumes.

Preamble

import Mathlib
open scoped Classical

Formal statement

namespace ShaoThreeUnits

theorem cauchy_davenport_chowla (p : ℕ) (hp : p.Prime)
    (I J K : Finset (ZMod p)) (hI : I.Nonempty) (hJ : J.Nonempty)
    (hK : K.Nonempty) (hsum : p + 2 ≤ I.card + J.card + K.card) (x : ZMod p) :
    ∃ u ∈ I, ∃ v ∈ J, ∃ w ∈ K, u + v + w = x := by sorry

end ShaoThreeUnits

Source

Xuancheng Shao, "A density version of the Vinogradov three primes theorem", Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2, https://arxiv.org/abs/1206.6139, the three-set form of Cauchy-Davenport used in Section 3

Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

Let p be a prime natural number, so ZMod p is the field with p elements. Fix three finite subsets I, J, and K of ZMod p, all nonempty, whose sizes satisfy |I| + |J| + |K| >= p + 2 in the natural numbers. The assertion is that every x in ZMod p can be written as u + v + w with u in I, v in J, and w in K. Equivalently, the threefold sumset I + J + K equals all of ZMod p, so it is a covering claim and not a lower bound on the sumset size. The threshold is the explicit value p + 2, with a non-strict inequality, and no constant is existentially quantified anywhere. The payload states the claim and leaves the proof as sorry.

QUANTIFIER ORDER p : N, universal, outermost. hp, primality of p. I, J, K, universal, finite subsets of ZMod p. hI, hJ, hK, nonemptiness of each set. hsum, the size bound. x : ZMod p, universal, after every set hypothesis. u, v, w, existential, innermost, so they may depend on x.

HYPOTHESES hp : p.Prime excludes p = 0, where ZMod 0 is the infinite ring of integers, and p = 1, where ZMod p is the zero ring. It also forces p >= 2 and caps each size at p. hI, hJ, hK exclude an empty factor. They are not implied by hsum: at p = 2, take I empty and J = K = ZMod 2, and then the size bound holds while the conclusion fails. hsum is stated in natural number arithmetic with addition only, so no truncated subtraction is involved. open scoped Classical supplies decidability instances and carries no mathematical content.

DEGENERATE CASES The hypotheses are satisfiable for every prime p, for instance I = J = K = ZMod p, since 3p >= p + 2 whenever p >= 1. So the statement is not vacuous. The bound does not force any set to be the whole field: at p = 5, sizes 3, 2, 2 satisfy it. The smallest instance is p = 2, where the three sizes must total at least 4 out of a maximum of 6. The quantified family of x is never empty, because ZMod p has p >= 2 elements, so the conclusion gets no free pass. Nothing here degenerates at an empty index range or a zero denominator.

UNREADABLE Nothing. Every binder, hypothesis, and symbol in the payload translated. The payload contains no auxiliary declaration, so no local name is left unexpanded.

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by aarontcao · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph