Long-Wagner Theorem 1.10 at $d = 3$ : the conjecture holds for unions of layers

Proved

Z2nFiveEighths.cubeFree_layerUnion_card_le_five_eighths

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

additive-combinatoricscombinatorics

For every $n \ge 4$ , a cube-free $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ that is a union of layers satisfies $8|A| \le 5 \cdot 2^n$ .

The layers partition $\mathbb{Z}/2^n\mathbb{Z}$ by 2-adic valuation: layer $i$ for $1 \le i \le n$ is the residues congruent to $2^{i-1}$ mod $2^i$ , and layer $n+1$ is $\{0\}$ . IsLayerUnion says that containing one element of a layer means containing all of it.

This is the largest class on which the conjectured constant is proved. The extremal set $L_1 \cup L_3$ lies in the class, so the restriction loses no sharpness.

Preamble

import Mathlib
import Definitions.Def_Z2nCubeFreeLayers

Formal statement

namespace Z2nFiveEighths

theorem cubeFree_layerUnion_card_le_five_eighths (n : ℕ) (hn : 4 ≤ n)
    (A : Finset (ZMod (2 ^ n))) (hlayer : IsLayerUnion n A) (hA : CubeFree A) :
    8 * A.card ≤ 5 * 2 ^ n := 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, Theorem 1.10, specialized to

d = 3

Read-back

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

READ-BACK

Fix an integer n with n at least 4 and work in the cyclic group Z/2^n. Each element x gets a level: if x = 0 the level is n+1, otherwise it is 1 plus the 2-adic valuation of the canonical representative of x in {1,...,2^n-1}. Levels therefore run 1 to n+1; level k for k at most n is the set of elements of valuation exactly k-1, of size 2^(n-k), and level n+1 is {0}. Let A be a finite subset of Z/2^n that is a union of whole levels: if it holds one element of a level it holds all of them. Assume further that A contains no triple x, y, z of elements of A, not required distinct and not required nonzero, for which x+y, y+z, z+x and x+y+z all lie in A as well. Conclusion: 8*|A| is at most 5*2^n, so |A| is at most (5/8)*2^n. The constant 5/8 is fixed, not existentially quantified, the inequality is non-strict, and it is stated as an integer inequality with no division.

QUANTIFIER ORDER n : natural number, universal, outermost. hn : 4 <= n. A : finite subset of Z/2^n, universal, after n. hlayer, hA : hypotheses on A. Inside the level condition: for all x, y in Z/2^n. Inside the forbidden configuration: there exist x, y, z in the group, negated, so the hypothesis reads as a universal statement over all triples.

HYPOTHESES hn rules out n <= 3, including the trivial ring at n = 0. hlayer rules out any A that splits a valuation class; it says x in A and level x = level y forces y in A. hA is the negation of the configuration condition. Since x = y = z = 0 is permitted, it forces 0 not in A, hence with hlayer A misses level n+1. Repeats are permitted generally: taking x = y = z = a it also forbids a, 2a, 3a all lying in A. AddCommGroup on the ambient type of the configuration definitions, instantiated at Z/2^n, which satisfies it; no constraint beyond commutative addition at the use site.

DEGENERATE CASES A empty satisfies both hypotheses and gives 0 <= 5*2^n, so the hypotheses are satisfiable and the statement is not vacuous. The set of all odd residues also satisfies both hypotheses and has size 2^(n-1) = (4/8)*2^n, so nonempty witnesses exist too. The convention padicValNat 2 0 = 0 is never reached, since x = 0 is branched out first.

UNREADABLE Nothing untranslated. One factual note: the target is closed by a placeholder proof, so the payload as given establishes 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

Long-Wagner Theorem 1.10 at d=3d = 3d=3: the conjecture holds for unions of layers

Long-Wagner Theorem 1.10 at $d = 3$ : the conjecture holds for unions of layers