Sharpness: the constant $\frac{5}{8}$ is attained for every $n \ge 3$

Proved

Z2nFiveEighths.five_eighths_attained

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

additive-combinatoricscombinatorics

For every $n \ge 3$ there is a cube-free $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ with $8|A| = 5 \cdot 2^n$ exactly.

The witness is $\{v : v \bmod 8 \in \{1,3,4,5,7\}\}$ , the odd residues together with those congruent to 4 mod 8, of size $2^{n-1} + 2^{n-3}$ . In Long and Wagner's layer notation this is $C_3 = L_1 \cup L_3$ .

This is what makes the conjecture a conjecture about a sharp constant rather than about some constant.

Preamble

import Mathlib
import Definitions.Def_Z2nCubeFreeLayers

Formal statement

namespace Z2nFiveEighths

theorem five_eighths_attained (n : ℕ) (hn : 3 ≤ n) :
    ∃ A : Finset (ZMod (2 ^ n)), 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, the construction

C_d

of Section 1

Read-back

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

READ-BACK

The statement asserts: for every natural number n with n at least 3, there is a finite subset A of the cyclic group of integers mod 2^n such that (i) A contains no triple with a certain closure property, and (ii) 8|A| = 52^n, i.e. |A| = 52^(n-3), exactly five eighths of the group. The forbidden configuration, written out, is: elements x, y, z, all three lying in A, such that x+y, y+z, z+x and x+y+z also all lie in A. So A is required to have the property that for no choice of three of its elements (repetition allowed) are all four of the listed sums again in A. The condition is a joint one on all seven values; it is not the requirement that A be closed-free under pairwise sums alone.

QUANTIFIER ORDER n : natural, universal, scopes over everything. hn : 3 <= n, universal hypothesis. A : Finset (ZMod (2^n)), existential, depends on n. Inside the forbidden configuration (negated): x, y, z : G, existential over the ambient group, then constrained to lie in A. Order among x, y, z is immaterial, and the negation makes this a universal statement about all triples.

HYPOTHESES hn : 3 <= n. Rules out n = 0, 1, 2. It is load-bearing rather than cosmetic: for n < 3 the natural-number equation 8|A| = 5*2^n has no solution, so without it the existential would be false at small n, not merely uninteresting. AddCommGroup G on the auxiliary definitions. Satisfied by ZMod (2^n) for every n, including n = 0, so it excludes nothing here. No distinctness hypothesis on x, y, z, and none on the seven listed values. Repetitions are permitted, which strengthens the condition imposed on A.

DEGENERATE CASES Taking x = y = z = 0 shows any A containing 0 has the forbidden configuration, so the required A must omit 0. Taking x = y = z = a shows the required A cannot contain a, 2a and 3a simultaneously for any a. A is nonempty: |A| = 52^(n-3) >= 5. The cardinality is exact equality, not a bound, and 52^(n-3) < 2^n, so it is achievable in principle by size alone. The statement is not vacuous: the hypothesis is satisfiable for every n >= 3, and the conclusion is an existence claim requiring a witness set.

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

Sharpness: the constant 58\frac{5}{8}85​ is attained for every n≥3n \ge 3n≥3

Sharpness: the constant $\frac{5}{8}$ is attained for every $n \ge 3$