The conjecture at $n = 4$

Proved

Z2nFiveEighths.cubeFree_card_le_five_eighths_four

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatorics

A cube-free $A \subseteq \mathbb{Z}/16\mathbb{Z}$ satisfies $8|A| \le 5 \cdot 16$ , that is $|A| \le 10$ .

The two constants differ at $n = 4$ but the integer maxima they admit coincide: $\frac{2}{3} \cdot 16 = 10.67$ and $\frac{5}{8} \cdot 16 = 10$ , and the two-thirds bound already forces $|A| \le 10$ . So this instance of the conjecture follows from the unconditional bound.

Preamble

import Mathlib
import Definitions.Def_Z2nCubeFreeLayers

Formal statement

namespace Z2nFiveEighths

theorem cubeFree_card_le_five_eighths_four (A : Finset (ZMod (2 ^ 4)))
    (hA : CubeFree A) : 8 * A.card ≤ 5 * 2 ^ 4 := by sorry

end Z2nFiveEighths

Source

Jason Long and Adam Zsolt Wagner, "The largest projective cube-free subsets of Z_{2^n}", arXiv:1810.01225, https://arxiv.org/abs/1810.01225, Conjecture 5.1 at

n = 4

Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

Let A be a finite subset of Z/16Z (written as the integers modulo 2^4 = 16, additive group). Say A contains a "full configuration" if there exist group elements x, y, z, not required to be distinct and not required to be nonzero, such that all seven nonempty subset sums of the triple lie in A: x, y, z, x+y, y+z, z+x, and x+y+z are each members of A. The first three conjuncts force x, y, z themselves into A, so the configuration is built from elements of A. The hypothesis is that A contains no such configuration. The conclusion is the natural-number inequality 8 * |A| <= 5 * 16 = 80, that is, |A| <= 10, which is exactly 5/8 of the order of the group. The statement concerns the single modulus 16 only; nothing is asserted for other powers of two, and the exponent 4 appears both in the modulus and in the right-hand constant. The auxiliary definitions are written for an arbitrary additive abelian group, but only the Z/16Z instance is used by the goal.

QUANTIFIER ORDER A: universally quantified finite subset of Z/16Z, outermost. hA: hypothesis about that A, second. x, y, z: existentially quantified over the ambient group, all three inside the scope of A, and all three inside the negation, so the hypothesis reads "for every x, y, z at least one of the seven memberships fails".

HYPOTHESES Typeclass [AddCommGroup G] on the two definitions: ambient carrier is an abelian group written additively; Z/16Z satisfies it. It rules out noncommutative or non-group carriers and does no other work at the instantiation used. hA: rules out every triple drawn from A whose three pairwise sums and whose total sum also lie in A. Since x = y = z is allowed, it forces 0 not in A (otherwise x = y = z = 0 works), and forbids any a in A with 2a and 3a also in A. Finiteness of A is automatic, the carrier has 16 elements.

DEGENERATE CASES A empty: hA holds vacuously, conclusion is 0 <= 80. The hypothesis is satisfiable with a large set: the 8 odd residues have all pairwise sums even, so hA holds there with |A| = 8. The theorem is therefore not vacuous. x, y, z may coincide and may be zero, so the forbidden configurations include the degenerate multiset cases noted above, not just three distinct elements. The conclusion is an exact inequality in the natural numbers, 8 * card <= 80, with no division and so no rounding ambiguity. No empty quantified family arises.

UNREADABLE nothing

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by aarontcao · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The conjecture at n=4n = 4n=4

The conjecture at $n = 4$