Shao's Proposition 3.2: the weighted case at
ProvedShaoThreeUnits.weighted_fifteenLet and let be the sum of over the eight units modulo 15. If
then every modulo 15 is a sum of three units with and .
The induction of Proposition 3.1 cannot reach this half. Shao's proof here is a linear program over the eight units.
import Mathlib open scoped Classical
namespace ShaoThreeUnits
theorem weighted_fifteen (f₁ f₂ f₃ : ZMod 15 → ℝ)
(h0 : ∀ x, 0 ≤ f₁ x ∧ 0 ≤ f₂ x ∧ 0 ≤ f₃ x)
(h1 : ∀ x, f₁ x ≤ 1 ∧ f₂ x ≤ 1 ∧ f₃ x ≤ 1)
(F₁ F₂ F₃ : ℝ)
(hF₁ : F₁ = ∑ x ∈ Finset.univ.filter (fun x : ZMod 15 => IsUnit x), f₁ x)
(hF₂ : F₂ = ∑ x ∈ Finset.univ.filter (fun x : ZMod 15 => IsUnit x), f₂ x)
(hF₃ : F₃ = ∑ x ∈ Finset.univ.filter (fun x : ZMod 15 => IsUnit x), f₃ x)
(hbig : 5 * (F₁ + F₂ + F₃) < F₁ * F₂ + F₂ * F₃ + F₃ * F₁) (x : ZMod 15) :
∃ a₁ : ZMod 15, IsUnit a₁ ∧ ∃ a₂ : ZMod 15, IsUnit a₂ ∧
∃ a₃ : ZMod 15, 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
Work in Z/15. Its units are the eight residues coprime to 15: 1, 2, 4, 7, 8, 11, 13, 14. Let f1, f2, f3 be real-valued functions defined on all of Z/15, each with values in the closed interval [0,1] at every residue (units and non-units alike). Let Fi be the sum of fi over the eight units only. Assume the strict inequality 5(F1+F2+F3) < F1F2 + F2F3 + F3F1. The claim: for every residue x mod 15 there exist units a1, a2, a3, not required distinct, with a1+a2+a3 = x in Z/15, with f1(a1)*f2(a2)*f3(a3) > 0, and with f1(a1)+f2(a2)+f3(a3) > 3/2. The constants 5 and 3/2 are fixed numerals, not existentially quantified. Since the values are nonnegative, the product condition says each of the three chosen values is strictly positive; that does not follow from the sum bound alone (1+1+0 exceeds 3/2 with product 0), so it is a genuine extra demand.
QUANTIFIER ORDER f1,f2,f3: universal, whole statement. h0, h1: for every residue, all 15, not just units. F1,F2,F3: universal reals, pinned by the three defining equations. x: universal over all of Z/15, bound after the largeness hypothesis. a1, then a2, then a3: existential, nested, chosen after x.
HYPOTHESES h0: nonnegativity everywhere; forbids cancellation inside the sums. h1: bounded by 1 everywhere; caps each Fi at 8. hF1, hF2, hF3: definitional, restricting the sums to the unit subset. Values at the seven non-units appear nowhere else in hypothesis or conclusion. hbig: strict quantitative largeness, coupling the three functions. Nothing else links f1, f2, f3. No typeclass constraints beyond the ring structure of Z/15 and classical decidability for the filter.
DEGENERATE CASES hbig is satisfiable: F1=F2=F3=8 gives 120 < 192, so the theorem is not vacuous. Strictness excludes equality cases. hbig does not force every Fi > 5: F1=F2=8, F3=2 satisfies it (90 < 96). hbig does force every Fi > 0: with F3=0 it needs 5(F1+F2) < F1F2, impossible for F1,F2 <= 8 (best case 80 < 64). So no branch where a function vanishes on all units. Every residue of Z/15 is a sum of three units (for instance 0 = 1+1+13), so no x is excluded for arithmetic reasons, and the conclusion is never unsatisfiable on those grounds alone. Behaviour of fi off the unit set is unconstrained beyond lying in [0,1], and the statement asserts nothing about it.
UNREADABLE Nothing.
Confirmed by the mission captain (proposal self-audit).