Shao's Proposition 3.1: the induction away from 3 and 5

Proved

ShaoThreeUnits.induction_coprime_thirty

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

additive-combinatoricsnumber-theory

Let $m$ be squarefree and coprime to 30, and let $f : \mathbb{Z}/m\mathbb{Z} \to [0,1]$ satisfy $\sum_{x \text{ unit}} f(x) > \frac{5}{8}\varphi(m)$ . Then every $x$ modulo $m$ is a sum $a + b + c$ of three units with

f(a)f(b) + f(b)f(c) + f(c)f(a) > \tfrac{5}{8}\big(f(a) + f(b) + f(c)\big).

The conclusion is stronger than it looks. It forces $f(a)$ , $f(b)$ and $f(c)$ all nonzero, and it is exactly the hypothesis that Proposition 3.2 consumes at the modulus 15.

Preamble

import Mathlib
open scoped Classical

Formal statement

namespace ShaoThreeUnits

theorem induction_coprime_thirty (m : ℕ) [NeZero m] (hsq : Squarefree m)
    (hcop : Nat.Coprime m 30) (f : ZMod m → ℝ) (h0 : ∀ x, 0 ≤ f x)
    (h1 : ∀ x, f x ≤ 1)
    (hsum : (5 : ℝ) / 8 * (Nat.totient m)
      < (∑ x ∈ Finset.univ.filter (fun x : ZMod m => IsUnit x), f x))
    (x : ZMod m) :
    ∃ a : ZMod m, IsUnit a ∧ ∃ b : ZMod m, IsUnit b ∧ ∃ c : ZMod m, IsUnit c ∧
      a + b + c = x ∧
      5 / 8 * (f a + f b + f c) < f a * f b + f b * f c + f c * f a := 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, Proposition 3.1

Read-back

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

READ-BACK

Let m be a natural number, nonzero by the instance assumption, squarefree, and coprime to 30, so m is either 1 or a product of distinct primes each at least 7. Let f be a real-valued function on the ring of residues mod m whose values lie in [0,1] at every residue, unit or not. Assume the sum of f over the group of units of that ring strictly exceeds (5/8) times Euler's totient of m, equivalently the average of f over the phi(m) units is strictly above 5/8. The claim: for every residue x, unit or not, there exist units a, b, c, not required to be distinct, with a + b + c = x and (5/8)(f(a) + f(b) + f(c)) < f(a)f(b) + f(b)f(c) + f(c)f(a). Both occurrences of 5/8 are real division by a fixed literal, not an existentially quantified constant, and both inequalities are strict.

QUANTIFIER ORDER m: universal, outermost, scopes everything. f: universal, after m, before all conditions on f. x: universal, after f and after every hypothesis, so a, b, c may depend on m, f, and x. a, then b, then c: existential, innermost, each paired with its own unit condition.

HYPOTHESES Nonzero-m instance: rules out m = 0, needed for the residue ring to be finite so the sum is over a finite set. Squarefree: no prime square divides m. Allows m = 1. Coprime to 30: gcd(m, 30) = 1, so 2, 3 and 5 do not divide m. On its own it also excludes m = 0. Lower and upper bound on f: 0 <= f <= 1 pointwise on all residues, including non-units, whose values appear nowhere else in the statement. Sum hypothesis: strict, and satisfiable, for instance by f identically 1, since phi(m) >= 1 and (5/8)phi(m) < phi(m). The theorem is therefore not vacuous.

DEGENERATE CASES m = 1: the ring is trivial, its single element 0 equals 1 and is a unit, phi(1) = 1, the sum hypothesis reads f(0) > 5/8, and the conclusion forces a = b = c = 0 = x, reducing to 5/8 < f(0). Live and consistent. The unit set is never empty, since 1 is always a unit, so the sum is never an empty sum compared against 0. x = 0 is permitted and is covered by the universal quantifier. If f vanished at all three chosen points the right side would be 0 and the strict inequality would fail, so the conclusion carries an implicit demand that f be positive on the witnesses.

UNREADABLE Nothing. Every binder translated. The proof body is omitted, so the payload carries a statement only.

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