The unconditional two-thirds bound

Proved

Z2nFiveEighths.cubeFree_card_le_two_thirds

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

additive-combinatoricscombinatorics

For every $n$ , a cube-free $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ satisfies $3|A| + 1 \le 2^{n+1}$ , so $|A| < \frac{2}{3}2^n$ .

This is the best unconditional constant available, and it should not be read as progress toward $\frac{5}{8}$ . Meng calls the two-thirds bound "quite trivial" and proves it in one paragraph for every cyclic group, not just for $\mathbb{Z}/2^n\mathbb{Z}$ .

The residual gap is exactly $\frac{2}{3} - \frac{5}{8} = \frac{1}{24}$ , so $2^n/24$ elements separate this from the conjecture.

Preamble

import Mathlib
import Definitions.Def_Z2nCubeFreeLayers

Formal statement

namespace Z2nFiveEighths

theorem cubeFree_card_le_two_thirds (n : ℕ) (A : Finset (ZMod (2 ^ n)))
    (hA : CubeFree A) : 3 * A.card + 1 ≤ 2 ^ (n + 1) := by sorry

end Z2nFiveEighths

Source

Yuchen Meng, "On Cube-Free Problems", Electron. J. Combin. 33(1) (2026) #P1.16, Theorem 9 together with the remark following its proof, which drops the hypothesis that 3 divides N and so covers N = 2^n; see also 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

Read-back

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

READ-BACK

The claim is: for every natural number n and every finite subset A of the additive group of integers modulo 2^n, if A contains no triple of the kind described below, then 3|A| + 1 <= 2^(n+1), that is |A| <= floor((2^(n+1) - 1)/3), a little under (2/3) of the ambient group of size 2^n. The forbidden configuration, written out in full (the local definition negated by the hypothesis), is: elements x, y, z, each a member of A, not required to be distinct, such that all four of x+y, y+z, z+x and x+y+z also lie in A. So the hypothesis says: for all x, y, z in A, at least one of the four sums x+y, y+z, z+x, x+y+z falls outside A. The bound is a fixed arithmetic inequality in n, with the constant 3 and the additive 1 stated explicitly; nothing is existentially quantified in the conclusion. The proof is a placeholder.

QUANTIFIER ORDER n : natural number, universal, scopes over everything. A : finite subset of Z/2^n Z, universal, depends on n. x, y, z inside the definition: existential in the forbidden configuration, hence universal once negated by the hypothesis; they range over the whole group but are pinned into A by explicit membership conjuncts, and are ordered x then y then z with no distinctness demanded.

HYPOTHESES hA: rules out any x, y, z in A (repeats allowed) whose three pairwise sums and total sum all lie in A. The diagonal case x = y = z = 0 makes all seven conjuncts read "0 in A", so hA forces 0 not in A. The case x = y = z = a forbids a, 2a, 3a all in A. The case x = y = a, z = b forbids a, b, 2a, a+b, 2a+b all in A. Typeclass AddCommGroup on the generic definitions; the theorem instantiates it at Z/2^n Z only, so commutativity and inverses are available and the ambient group is cyclic of 2-power order. No hypothesis n >= 1. Arithmetic in the conclusion is over the naturals, so no truncated subtraction appears.

DEGENERATE CASES A empty: hA holds with nothing to check, conclusion reads 1 <= 2^(n+1), true. n = 0: the group is trivial, A is empty or {0}; {0} violates hA, so only the empty case survives and the bound reads 1 <= 2. n = 1: hA permits A = {1}, and the bound 3+1 <= 4 is met with equality. The hypothesis is satisfiable for every n >= 1 (for instance the odd residues), so the statement is not vacuous.

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