Divisor reduction: the weighted result descends to every divisor
ProvedShaoThreeUnits.divisor_reductionThe weighted local result stated for a single modulus implies the same statement for every divisor of .
This is the opening move in the proof of Proposition 1.4. It is what lets the proof assume without loss of generality, by passing from to and pulling the conclusion back along the reduction map.
Both halves of the implication are the statement of the weighted local result with the modulus fixed, written out in full here because a mission item carries no definitions of its own.
import Mathlib open scoped Classical
namespace ShaoThreeUnits
theorem divisor_reduction (m M : ℕ) [NeZero m] [NeZero M] (hdvd : m ∣ M)
(hM : ∀ g : ZMod M → ℝ, (∀ x, 0 ≤ g x) → (∀ x, g x ≤ 1) →
(5 : ℝ) / 8 * (Nat.totient M)
< (∑ x ∈ Finset.univ.filter (fun x : ZMod M => IsUnit x), g x) →
∀ y : ZMod M, ∃ b₁ : ZMod M, IsUnit b₁ ∧ ∃ b₂ : ZMod M, IsUnit b₂ ∧
∃ b₃ : ZMod M, IsUnit b₃ ∧ b₁ + b₂ + b₃ = y ∧
0 < g b₁ * g b₂ * g b₃ ∧ 3 / 2 < g b₁ + g b₂ + g b₃) :
∀ f : ZMod m → ℝ, (∀ x, 0 ≤ f x) → (∀ x, f x ≤ 1) →
(5 : ℝ) / 8 * (Nat.totient m)
< (∑ x ∈ Finset.univ.filter (fun x : ZMod m => IsUnit x), f x) →
∀ y : ZMod m, ∃ a₁ : ZMod m, IsUnit a₁ ∧ ∃ a₂ : ZMod m, IsUnit a₂ ∧
∃ a₃ : ZMod m, IsUnit a₃ ∧ a₁ + a₂ + a₃ = y ∧
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
Write P(N) for this property of a modulus N: for every real-valued function g on Z/N with 0 <= g(x) <= 1 at every x, if the sum of g over the units of Z/N is strictly greater than (5/8)*phi(N), phi being Euler's totient, then for every y in Z/N there exist units b1, b2, b3 of Z/N, not required to be distinct, with b1+b2+b3 = y, with g(b1)g(b2)g(b3) > 0, and with g(b1)+g(b2)+g(b3) > 3/2. Because g is nonnegative, the product condition says exactly that each of the three values is strictly positive. The theorem fixes nonzero naturals m and M with m dividing M and asserts: P(M) implies P(m). That is, the property descends from a multiple to a divisor. No ring map or reduction between Z/M and Z/m appears anywhere in the statement; the two instances are joined only by the divisibility hypothesis. Both constants are literal and identical at the two moduli: the mass threshold is 5/8 times the totient, the value threshold is 3/2, and both comparisons are strict.
QUANTIFIER ORDER m, M and the divisibility fixed at the outside. Inside P(N): g universal, first. Then the three pointwise and mass hypotheses on g. Then y universal, after g. Then b1, then b2, then b3 existential, each allowed to depend on g and y. P(M) is the single hypothesis; P(m) is the conclusion.
HYPOTHESES NeZero m and NeZero M: rules out modulus 0, where Z/0 is the integers; it is also what makes Z/N finite, so the sum over units is defined. m divides M: the only link between moduli. It permits m = M, where hypothesis and conclusion are the same sentence. 0 <= g and g <= 1: imposed at every point, units and non-units alike; values at non-units occur nowhere else. Mass condition: strict inequality, so equality at (5/8)phi(N) gives nothing. hM is assumed for the one fixed M only, not for all multiples of m.
DEGENERATE CASES Modulus 1: Z/1 is the zero ring, its single element is a unit, phi(1) = 1; the mass condition reads 5/8 < g(0) and the conclusion holds with all three units equal to 0. Not vacuous: g identically 1 satisfies the mass condition at every N >= 1, since phi(N) > (5/8)phi(N). The unit set is never empty for N >= 1. The three units may coincide, so the conclusion can be met by one unit b with 3b = y and g(b) > 1/2.
UNREADABLE nothing
Confirmed by the mission captain (proposal self-audit).