The conjecture at
ProvedZ2nFiveEighths.cubeFree_card_le_five_eighths_fiveA cube-free satisfies , that is .
Unlike , counting is not enough here. The two-thirds bound gives , and the last element has to be excluded by a structural argument about which residues can coexist.
import Mathlib import Definitions.Def_Z2nCubeFreeLayers
namespace Z2nFiveEighths
theorem cubeFree_card_le_five_eighths_five (A : Finset (ZMod (2 ^ 5)))
(hA : CubeFree A) : 8 * A.card ≤ 5 * 2 ^ 5 := by sorry
end Z2nFiveEighths
Read-back
What the Lean code literally says, in plain math · claude-opus-5
READ-BACK
Let A be a finite subset of the cyclic group of integers modulo 2^5 = 32 (written additively). Call a finite subset A of an additive abelian group "rich" if there exist group elements x, y, z, all three lying in A, such that the four further elements x+y, y+z, z+x and x+y+z also all lie in A. The hypothesis is that A is not rich: for every choice of x, y, z in A (not required to be distinct, not required to be nonzero), at least one of x+y, y+z, z+x, x+y+z falls outside A. The conclusion is 8*|A| <= 5*32 = 160 in the natural numbers, that is |A| <= 20, exactly five eighths of the 32 elements of the ambient group. The modulus is the fixed number 2^5; nothing here is quantified over an exponent, and the ratio 5/8 is a fixed constant, not an unspecified one.
QUANTIFIER ORDER aux1: universally over the group type G and its abelian group structure, then over the finite set A; body is existential over x, then y, then z in G, all three in one block, scope the seven membership conditions. aux2 is literally the negation of aux1 at the same A, so its three variables become universal. target: universally over A, a finite subset of the integers mod 32; then the hypothesis; then the cardinality bound. No existential in the conclusion.
HYPOTHESES [AddCommGroup G] on the two definitions: commutativity and associativity are used freely in reading x+y+z, and the group is written additively. Instantiated at the integers mod 32, which qualifies. hA, the non-richness condition: rules out, among other things, 0 in A (take x = y = z = 0), and rules out any a in A having both 2a and 3a in A (take x = y = z = a). Also rules out, for a, b in A, the pattern a+b, 2a, 2a+b all in A (take z = x). No distinctness, nonzero, symmetry, or nonemptiness condition is imposed on A.
DEGENERATE CASES A empty: the hypothesis holds vacuously and the conclusion reads 0 <= 160, so the statement is true for free there. A a nonzero singleton: hypothesis holds (2a = a forces a = 0), so the hypothesis is satisfiable by nonempty sets and the theorem is not vacuous. The 16 odd residues satisfy the hypothesis (a sum of two odd elements is even), so sets of size 16 are admissible and the bound 20 is not trivially unreachable. The ambient type has 32 elements, so |A| <= 32 holds automatically; the assertion is the strengthening to 20.
UNREADABLE nothing.
Confirmed by the mission captain (proposal self-audit).