Shao's Proposition 1.4: the weighted local result
ProvedShaoThreeUnits.weighted_local_resultLet be an odd squarefree positive integer and let satisfy . Then every modulo can be written with units, and .
The main theorem is the case of this. The induction cannot be run on sets, because passing from to a prime factor splits into fibers of different densities, so the whole proof is carried by functions into .
The constant is sharp. Take , , and , which forces the multiset and gives the sum exactly .
import Mathlib open scoped Classical
namespace ShaoThreeUnits
theorem weighted_local_result (m : ℕ) [NeZero m] (hodd : Odd m)
(hsq : Squarefree m) (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₁ ∧ ∃ a₂ : ZMod m, IsUnit a₂ ∧
∃ a₃ : ZMod m, IsUnit a₃ ∧ a₁ + a₂ + a₃ = x ∧
0 < f a₁ * f a₂ * f a₃ ∧ 3 / 2 < f a₁ + f a₂ + f a₃ := by sorry
end ShaoThreeUnits
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Let m be a positive odd squarefree natural number, and let f be a real-valued function on the residues mod m taking values in the closed interval [0,1] at every residue (not only at the invertible ones). Assume the total weight carried by the invertible residues, the sum of f(u) over all units u of Z/mZ, exceeds (5/8) phi(m), where phi is Euler's totient, that is, the number of units. Then for every residue x mod m, whether or not x is invertible, there exist three units a1, a2, a3 (not required to be distinct) with a1 + a2 + a3 = x, with f(a1) f(a2) f(a3) > 0, and with f(a1) + f(a2) + f(a3) > 3/2. The product condition is not implied by the sum condition: since each value is at most 1, a sum above 3/2 forces at least two of the three values to be positive but allows the third to vanish, so requiring the product to be positive additionally forbids any of the three from being zero. The constants are exactly 5/8 in the hypothesis and exactly 3/2 in the conclusion, both fixed rather than existentially quantified, and both inequalities are strict. Equivalently the hypothesis says the mean of f over the units exceeds 5/8 while the conclusion demands a triple whose mean exceeds 1/2. The proof body is a sorry, so the file asserts the statement and establishes nothing.
QUANTIFIER ORDER m : natural number, outermost, universal. NeZero m : typeclass, m nonzero. hodd, hsq : hypotheses on m. f : function from Z/mZ to the reals, universal, after m. h0, h1, hsum : hypotheses on f. x : residue mod m, universal, and it comes before the existentials, so the triple may depend on x. a1, a2, a3 : existential, innermost, each carrying its own invertibility clause.
HYPOTHESES NeZero m : rules out m = 0, and is what makes Z/mZ finite so the sum over units is defined. hodd : m odd. Rules out even m, where a sum of three units is forced into one parity class and cannot hit every x. hsq : m squarefree. Rules out any m divisible by a square, and also rules out m = 0 again. h0 : f is nonnegative everywhere on Z/mZ. h1 : f is at most 1 everywhere on Z/mZ. With h0 this caps the unit sum at phi(m). hsum : strict lower bound (5/8) phi(m) on the unit sum. Classical choice is opened only so that invertibility can be used as a filter.
DEGENERATE CASES m = 1 is admitted: 1 is odd, squarefree and nonzero. Z/1Z is the zero ring, its single element is a unit, phi(1) = 1, so the hypothesis reads f(0) > 5/8 and the conclusion is satisfied by a1 = a2 = a3 = 0. The hypotheses are jointly satisfiable for every admissible m, for instance f identically 1, since phi(m) >= 1 > (5/8) phi(m). So the theorem is not vacuous. The unit set is never empty and phi(m) is never 0 under these hypotheses. Values of f off the units are constrained by h0 and h1 but appear nowhere else.
UNREADABLE nothing
Confirmed by the mission captain (proposal self-audit).