Shao's Corollary 1.5: density forces
ProvedShaoThreeUnits.three_units_of_five_eighthsLet be an odd squarefree positive integer and let be a set every element of which is a unit. If , then every residue class modulo , unit or not, can be written with not necessarily distinct. Equivalently .
The size hypothesis is written 5 * Nat.totient m < 8 * A.card, which is cleared of division so the statement stays in with no rounding.
The constant is sharp and the inequality has to be strict: at the set has five elements, so exactly, and is not a sum of three of its elements.
import Mathlib open scoped Classical
namespace ShaoThreeUnits
theorem three_units_of_five_eighths
(m : ℕ) [NeZero m] (hodd : Odd m) (hsq : Squarefree m)
(A : Finset (ZMod m)) (hA : ∀ a ∈ A, IsUnit a)
(hcard : 5 * Nat.totient m < 8 * A.card) (x : ZMod m) :
∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a + b + c = x := by sorry
end ShaoThreeUnits
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
For every natural number m that is odd and squarefree, and every finite set A of residues mod m all of whose elements are invertible mod m (coprime to m), if the size of A satisfies 5phi(m) < 8|A|, that is |A| > (5/8)*phi(m) with phi Euler's totient, then every residue x mod m can be written as a sum of three elements of A: there exist a, b, c in A with a + b + c = x. The three elements are chosen independently and are not required to be distinct, so a = b = c is permitted; no uniqueness or counting of representations is asserted. The threshold constant is exactly 5/8 and the inequality on it is strict, and it is a fixed constant rather than an existentially quantified one. Odd plus squarefree means m is a product of distinct odd primes (m = 1 allowed).
QUANTIFIER ORDER m : natural number, universal, scopes over everything. Instance NeZero m, i.e. m is nonzero. hodd, hsq: hypotheses on m. A: finite set of residues mod m, universal, chosen after m and before x. hA, hcard: hypotheses on A. x: residue mod m, universal, chosen after A. So one A must work for all x simultaneously. a, b, c: existential, innermost, may depend on m, A and x, each ranging over A.
HYPOTHESES NeZero m: rules out m = 0. Redundant given the next two (Odd 0 and Squarefree 0 are both false), so it adds no constraint. hodd (Odd m): rules out even m, in particular m = 2 and all m divisible by 2. hsq (Squarefree m): rules out any m divisible by the square of a prime, e.g. 9, 27, 45. hA: every element of A is a unit of Z/mZ; rules out any A containing a residue sharing a factor with m. This caps |A| at phi(m). hcard: rules out A of size at most (5/8)phi(m); combined with the cap, A occupies strictly more than five eighths of the unit group. No typeclass beyond NeZero. Ambient classical logic is opened but nothing depends on it in the statement.
DEGENERATE CASES A empty is impossible: phi(m) >= 1, so hcard forces |A| >= 1. m = 1 satisfies all hypotheses; Z/1Z is the one-element ring, phi(1) = 1, hcard forces A = {0}, and 0 + 0 + 0 = 0 = x, so the case is true but empty of content. The hypotheses are jointly satisfiable for many m (1, 3, 5, 7, 15, ...), so the statement is not vacuous. x = 0 is included, and is met by any a, b, c in A summing to zero; nothing excludes it.
UNREADABLE nothing.
Confirmed by the mission captain (proposal self-audit).