Shao's Lemma 2.3: the finite check at $m = 15$

Proved

ShaoThreeUnits.finite_check_fifteen

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

additive-combinatoricsnumber-theory

Let $A$ , $B$ , $C$ be sets of units modulo 15. If

|A||B| + |B||C| + |C||A| > 5(|A| + |B| + |C|)

then every residue $x$ modulo 15 can be written $x = a + b + c$ with $a \in A$ , $b \in B$ and $c \in C$ .

There are eight units modulo 15, so the hypothesis is a finite condition on three integers in $[0,8]$ . Thirty-four unordered size triples satisfy it, of which $(2,7,8)$ , $(3,6,7)$ , $(4,5,7)$ , $(4,6,6)$ and $(5,5,6)$ are the minimal ones under componentwise order.

Preamble

import Mathlib
open scoped Classical

Formal statement

namespace ShaoThreeUnits

theorem finite_check_fifteen (A B C : Finset (ZMod 15))
    (hA : ∀ a ∈ A, IsUnit a) (hB : ∀ b ∈ B, IsUnit b)
    (hC : ∀ c ∈ C, IsUnit c)
    (hsize : 5 * (A.card + B.card + C.card)
      < A.card * B.card + B.card * C.card + C.card * A.card) (x : ZMod 15) :
    ∃ a ∈ A, ∃ b ∈ B, ∃ c ∈ C, a + b + c = 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, Lemma 2.3

Read-back

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

READ-BACK

Work in the ring of integers mod 15. The statement takes three finite subsets A, B, C of Z/15Z all of whose elements are invertible, hence coprime to 15, so each is contained in the 8-element unit group {1,2,4,7,8,11,13,14} and has at most 8 elements. Under the strict cardinality inequality 5(|A|+|B|+|C|) < |A||B| + |B||C| + |C||A| (coefficient exactly 5, strict, all arithmetic in the naturals so no truncated subtraction arises), the claim is that every x in Z/15Z is representable as x = a + b + c with a in A, b in B, c in C. The conclusion imposes no distinctness on a, b, c, does not restate that they are units (that follows from membership), and constrains A, B, C only by size, not by structure.

QUANTIFIER ORDER A, B, C: universal, outermost, scope is the whole statement. hA, hB, hC, hsize: hypotheses on A, B, C, in that order. x: universal, an element of Z/15Z, bound after hsize; since hsize does not mention x, this is a plain "for every x". a, then b, then c: existential, inside the conclusion, chosen after x, so each may depend on x.

HYPOTHESES hA, hB, hC: membership implies unit. Excludes 0, 3, 5, 6, 9, 10, 12 from each set, capping every cardinality at 8. hsize: combined with that cap it forces each of |A|, |B|, |C| to be at least 2 (size 0 or 1 makes the inequality unsatisfiable even when the other two sets are the full unit group). It rules out small size triples, for instance (5,5,5) gives 75 < 75, false. It is satisfiable: (6,6,6) gives 90 < 108, and (2,8,8) gives 90 < 96. So the theorem is not vacuous. No typeclass constraints appear beyond what Finset over a finite type supplies. The Classical scope only provides decidability instances and does not change the content.

DEGENERATE CASES Empty A, B or C: excluded by hsize, since with one set empty the right side is at most 64 while the left is at least 80. So the existential never ranges over an empty set. x = 0 is included among the targets, as are all 15 residues, units and non-units alike. The hypothesis is a purely numerical condition on three integers each in [0,8], so it is a finite check; it is satisfiable, so no vacuity.

UNREADABLE Nothing. There are no auxiliary declarations, and the proof body is a placeholder, so there is no proof content to read.

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

Shao's Lemma 2.3: the finite check at m=15m = 15m=15

Shao's Lemma 2.3: the finite check at $m = 15$